\documentclass{article}
\usepackage{czt}

\begin{document}
\begin{zsection}
  \SECTION zTime \parents standard\_toolkit
\end{zsection}

\begin{zed}
  [CONTEXT, TASK]
\end{zed}

\begin{axdef}
  bare\_context: CONTEXT\\
  idle: TASK
\end{axdef}

\begin{zed}
STATE ::= nonexistent | ready | blocked | suspended | running
\end{zed}

\begin[disabled]{zed}
transition == (\{blocked\} \cross  \{nonexistent, ready, running, suspended\}) \cup  (\{nonexistent\} \cross  \{ready, running\}) \cup  (\{ready\} \cross  \{nonexistent, running, suspended\}) \cup  (\{running\} \cross  \{blocked, nonexistent, ready, suspended\}) \cup  (\{suspended\} \cross  \{nonexistent, ready, running\})
\end{zed}

\begin{theorem}{grule gTransitionType}
transition \in  \power  (STATE \cross  STATE)
\end{theorem}

\begin{zproof}[gTransitionType]
with enabled (transition) prove by reduce;
\end{zproof}

\begin{theorem}{rule lInTransition}
\forall  l, r: STATE | (l, r) \in  \{nonexistent \mapsto  ready, running \mapsto  ready, blocked \mapsto  ready, suspended \mapsto  ready, ready \mapsto  running, blocked \mapsto  running, suspended \mapsto  running, nonexistent \mapsto  running, running \mapsto  suspended, ready \mapsto  suspended, blocked \mapsto  suspended, running \mapsto  blocked, running \mapsto  nonexistent, ready \mapsto  nonexistent, blocked \mapsto  nonexistent, suspended \mapsto  nonexistent\} @ (l, r) \in  transition
\end{theorem}

\begin{zproof}[lInTransition]
with normalization with enabled (transition) prove by reduce;
\end{zproof}

\begin{schema}{TaskData}
  tasks: \finset  TASK\\
  running\_task: TASK
\where
  running\_task \in  tasks\\
  idle \in  tasks
\end{schema}

\begin{schema}{Init\_TaskData}
  TaskData~'
\where
  tasks' = \{idle\}\\
  running\_task' = idle
\end{schema}

\begin{theorem}{TaskDataInit}
\exists  TaskData~' @ Init\_TaskData
\end{theorem}

\begin{zproof}[TaskDataInit]
prove by reduce;
\end{zproof}

\begin{schema}{StateData}
  state: TASK \fun  STATE
\where
  state(idle) \in  \{ready, running\}
\end{schema}

\begin{schema}{Init\_StateData}
  StateData~'
\where
  state' = (\lambda  x: TASK @ nonexistent) \oplus  \{(idle \mapsto  running)\}
\end{schema}

\begin{theorem}{StateDataInit}
\exists  StateData~' @ Init\_StateData
\end{theorem}

\begin{zproof}[StateDataInit]
prove by reduce;
\end{zproof}

\begin{schema}{ContextData}
  phys\_context: CONTEXT\\
  log\_context: TASK \fun  CONTEXT
\end{schema}

\begin{schema}{Init\_ContextData}
  ContextData~'
\where
  phys\_context' = bare\_context\\
  log\_context' = (\lambda  x: TASK @ bare\_context)
\end{schema}

\begin{theorem}{ContextDataInit}
\exists  ContextData~' @ Init\_ContextData
\end{theorem}

\begin{zproof}[ContextDataInit]
prove by reduce;
\end{zproof}

\begin{schema}{PrioData}
  priority: TASK \fun  \nat 
\where
  priority(idle) = 0
\end{schema}

\begin{schema}{Init\_PrioData}
  PrioData~'
\where
  priority' = (\lambda  x: TASK @ 0)
\end{schema}

\begin{theorem}{PrioDataInit}
\exists  PrioData~' @ Init\_PrioData
\end{theorem}

\begin{zproof}[PrioDataInit]
prove by reduce;
\end{zproof}

\begin{schema}{Task}
  TaskData\\
  StateData\\
  ContextData\\
  PrioData
\where
  tasks = TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg )\\
  state \inv  \limg  \{running\} \rimg  = \{running\_task\}\\
  \forall  pt: state \inv  \limg  \{ready\} \rimg  @ priority(running\_task) \geq  priority(pt)
\end{schema}

\begin{schema}{\Delta Task}
  Task\\
  Task~'
\where
  \forall  st: TASK | state'(st) \neq  state(st) @ state(st) \mapsto  state'(st) \in  transition
\end{schema}

\begin{axdef}
  f: \power  TASK \fun  TASK
\where
  \Label{findDelegate}
  \forall  Task; a: \power  TASK; g: TASK \pfun \num @ \\
  f(a) \in  a \land a \subseteq \dom g \land\\
  (\forall  t: a @ g (f(a)) \geq  g (t))
\end{axdef}

\begin{zproof}[f\$domainCheck]
prove;
\end{zproof}

\begin{theorem}{TaskProperty1}
\forall  Task @ state(running\_task) = running
\end{theorem}

\begin{zproof}[TaskProperty1]
invoke Task;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
rewrite;
\end{zproof}

\begin{theorem}{TaskProperty2}
\forall  Task @ \forall  t: TASK | t \in  state \inv  \limg  \{blocked\} \rimg  @ t \in  tasks
\end{theorem}

\begin{zproof}[TaskProperty2]
invoke Task;
prove;
\end{zproof}

\begin{theorem}{TaskProperty3}
\forall  Task @ \forall  t: state \inv  \limg  \{ready\} \rimg  @ t \in  tasks \setminus  \{running\_task\}
\end{theorem}

\begin{zproof}[TaskProperty3]
invoke Task;
prove;
\end{zproof}

\begin{theorem}{TaskProperty6}
\forall  Task; t: TASK | 0 < priority(t) @ idle \neq  t
\end{theorem}

\begin{zproof}[TaskProperty6]
prove by reduce;
\end{zproof}

\begin{schema}{Init\_Task}
  Task~'
\where
  Init\_TaskData\\
  Init\_StateData\\
  Init\_ContextData\\
  Init\_PrioData
\end{schema}

\begin{theorem}{TaskInit}
\exists  Task~' @ Init\_Task
\end{theorem}

\begin{zproof}[TaskInit]
prove by reduce;
apply extensionality;
prove;
apply applyOverride1;
prove;
\end{zproof}

\begin{schema}{Reschedule}
  \Delta Task\\
  target?: TASK\\
  tasks?: \finset  TASK\\
  st?: STATE\\
  pri?: TASK \fun  \nat 
\where
  tasks' = tasks?\\
  running\_task' = target?\\
  state' = state \oplus  \{(target? \mapsto  running), (running\_task \mapsto  st?)\}\\
  phys\_context' = log\_context(target?)\\
  log\_context' = log\_context \oplus  \{(running\_task \mapsto  phys\_context)\}\\
  priority' = pri?
\end{schema}

\begin{zed}
disableReschedule \defs [Task | false] \land  Reschedule
\end{zed}

\begin{schema}{CreateTaskN\_T}
  \Delta Task\\
  target?: TASK\\
  newpri?: \nat 
\where
  state(target?) = nonexistent\\
  newpri? \leq  priority(running\_task)\\
  tasks' = tasks \cup  \{target?\}\\
  running\_task' = running\_task\\
  state' = state \oplus  \{(target? \mapsto  ready)\}\\
  \Xi ContextData\\
  priority' = priority \oplus  \{(target? \mapsto  newpri?)\}
\end{schema}

\begin{schema}{CreateTaskN\_TFSBSig}
  Task\\
  target?: TASK\\
  newpri?: \nat 
\where
  state(target?) = nonexistent\\
  newpri? \leq  priority(running\_task)
\end{schema}

\begin{theorem}{rule runningUpdate}
\forall  f: TASK \fun  STATE; g: TASK \pfun  STATE | running \notin  \ran  g \land  (f \inv  \limg  \{running\} \rimg ) \cap  \dom  g = \emptyset @ (f \oplus  g) \inv  \limg  \{running\} \rimg  = f \inv  \limg  \{running\} \rimg 
\end{theorem}

\begin{zproof}[runningUpdate]
apply extensionality to predicate (f \oplus  g) \inv  \limg  \{running\} \rimg  = f \inv  \limg  \{running\} \rimg ;
prove;
cases;
split x \in  \dom  g;
prove;
use applyInRanPfun[TASK, STATE][A := TASK, B := STATE, f := g, a := x];
prove;
next;
apply applyOverride to expression (f \oplus  g) y;
prove;
apply extensionality to predicate \dom  g \cap  (f \inv  \limg  \{running\} \rimg ) = \{\};
prove;
instantiate x == y;
prove;
next;
\end{zproof}

\begin{theorem}{rule setminUpdate}
\forall  f: TASK \fun  STATE; g: TASK \pfun  STATE @ TASK \setminus  ((f \oplus  g) \inv  \limg  \{nonexistent\} \rimg ) = TASK \setminus  (f \inv  \limg  \{nonexistent\} \rimg ) \setminus  (g \inv  \limg  \{nonexistent\} \rimg ) \cup  (\dom  g \setminus  (g \inv  \limg  \{nonexistent\} \rimg ))
\end{theorem}

\begin{zproof}[setminUpdate]
apply extensionality to predicate TASK \setminus  ((f \oplus  g) \inv  \limg  \{nonexistent\} \rimg ) = TASK \setminus  (f \inv  \limg  \{nonexistent\} \rimg ) \setminus  (g \inv  \limg  \{nonexistent\} \rimg ) \cup  (\dom  g \setminus  (g \inv  \limg  \{nonexistent\} \rimg ));
prove;
with normalization reduce;
split x \in  \dom  g;
prove;
\end{zproof}

\begin{theorem}{CreateTaskN\_T\_vc\_ref}
\forall  CreateTaskN\_TFSBSig | true @ \pre  CreateTaskN\_T
\end{theorem}

\begin{zproof}[CreateTaskN\_T\_vc\_ref]
with disabled (ContextData) prove by reduce;
instantiate pt\_\_0 == pt;
with enabled (applyOverride) prove;
apply applyOverride;
with normalization reduce;
\end{zproof}

\begin{schema}{CreateTaskS\_T}
  \Delta Task\\
  target?: TASK\\
  newpri?: \nat 
\where
  state(target?) = nonexistent\\
  newpri? > priority(running\_task)\\
  \exists  st?: STATE; tasks?: \finset  TASK; pri?: TASK \fun  \nat  | st? = ready \land  tasks? = tasks \cup  \{target?\} \land  pri? = priority \oplus  \{(target? \mapsto  newpri?)\} @ Reschedule
\end{schema}

\begin{schema}{CreateTaskS\_TFSBSig}
  Task\\
  target?: TASK\\
  newpri?: \nat 
\where
  state(target?) = nonexistent\\
  newpri? > priority(running\_task)
\end{schema}

\begin{theorem}{CreateTaskS\_T\_vc\_ref}
\forall  CreateTaskS\_TFSBSig | true @ \pre  CreateTaskS\_T
\end{theorem}

\begin{zproof}[CreateTaskS\_T\_vc\_ref]
prove by reduce;
apply applyOverride to expression (state \oplus  (\{(running\_task, ready)\} \cup  \{(target?, running)\})) idle;
prove;
cases;
apply extensionality to predicate (state \oplus  (\{(running\_task, ready)\} \cup  \{(target?, running)\})) \inv  \limg  \{running\} \rimg  = \{target?\};
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
prove;
instantiate x\_\_0 == x;
prove;
apply applyOverride;
prove;
split x \in  TASK;
split x = running\_task;
prove;
next;
apply extensionality to predicate TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ) \cup  ((state \inv  \limg  \{running\} \rimg ) \cup  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(target?, running)\})) \inv  \limg  \{running\} \rimg )) = TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ) \cup  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(target?, running)\})) \inv  \limg  \{running\} \rimg );
prove;
apply applyOverride;
prove;
next;
apply applyOverride;
prove;
split pt = running\_task;
prove;
instantiate pt\_\_0 == pt;
prove;
next;
apply applyOverride;
prove;
with normalization prove;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
instantiate y == st;
prove;
next;
\end{zproof}

\begin{zed}
CreateTask\_T \defs CreateTaskN\_T \lor  CreateTaskS\_T
\end{zed}

\begin{schema}{DeleteTaskN\_T}
  \Delta Task\\
  target?: TASK\\
  topReady!: TASK
\where
  target? \in  tasks \setminus  \{idle\}\\
  state(target?) \in  \{ready, blocked, suspended\}\\
  tasks' = tasks \setminus  \{target?\}\\
  running\_task' = running\_task\\
  state' = state \oplus  \{(target? \mapsto  nonexistent)\}\\
  phys\_context' = phys\_context\\
  log\_context' = log\_context \oplus  \{(target? \mapsto  bare\_context)\}\\
  \Xi PrioData\\
  topReady! = running\_task
\end{schema}

\begin{schema}{DeleteTaskN\_TFSBSig}
  Task\\
  target?: TASK
\where
  target? \in  tasks \setminus  \{idle\}\\
  state(target?) \in  \{ready, blocked, suspended\}
\end{schema}

\begin{theorem}{finsetIsFinset}
\forall  X: \finset  TASK; x: TASK @ X \setminus  \{x\} \in  \finset  TASK
\end{theorem}

\begin{zproof}[finsetIsFinset]
prove;
\end{zproof}

\begin{theorem}{DeleteTaskN\_T\_vc\_ref}
\forall  DeleteTaskN\_TFSBSig | true @ \pre  DeleteTaskN\_T
\end{theorem}

\begin{zproof}[DeleteTaskN\_T\_vc\_ref]
prove by reduce;
use finsetIsFinset[X := TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ), x := target?];
prove;
apply extensionality to predicate (state \oplus  \{(target?, nonexistent)\}) \inv  \limg  \{running\} \rimg  = state \inv  \limg  \{running\} \rimg ;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
prove;
apply applyOverride;
instantiate pt\_\_0 == pt;
split state(target?) = ready;
prove;
split state(target?) = blocked;
prove;
\end{zproof}

\begin{schema}{DeleteTaskS\_T}
  \Delta Task\\
  target?: TASK\\
  topReady!: TASK
\where
  target? \in  tasks \setminus  \{idle\}\\
  state(target?) \in  \{running\}\\
  state(topReady!) = ready\\
  \forall  t: state \inv  \limg  \{ready\} \rimg  @ priority(topReady!) \geq  priority(t)\\
  tasks' = tasks \setminus  \{target?\}\\
  running\_task' = topReady!\\
  state' = state \oplus  \{(topReady! \mapsto  running), (target? \mapsto  nonexistent)\}\\
  phys\_context' = log\_context(topReady!)\\
  log\_context' = log\_context \oplus  \{(target? \mapsto  bare\_context)\}\\
  \Xi PrioData
\end{schema}

\begin{schema}{DeleteTaskS\_TFSBSig}
  Task\\
  target?: TASK
\where
  target? \in  tasks \setminus  \{idle\}\\
  state(target?) \in  \{running\}
\end{schema}

\begin{theorem}{lDeleteTaskS\_T\_Lemma}
\forall  Task; topReady!, target?: TASK | target? \in  tasks \setminus  \{idle\} \land  state(target?) \in  \{running\} \land  state(topReady!) = ready \land  (\forall  rtsk: state \inv  \limg  \{ready\} \rimg  @ priority(topReady!) \geq  priority(rtsk)) @ \lnot  (Task[log\_context := log\_context \oplus  \{(target?, bare\_context)\}, phys\_context := log\_context(topReady!), running\_task := topReady!, state := state \oplus  (\{(target?, nonexistent)\} \cup  \{(topReady!, running)\}), tasks := tasks \setminus  \{target?\}] \land  (st \in  TASK \land  \lnot  (state \oplus  (\{(target?, nonexistent)\} \cup  \{(topReady!, running)\}))(st) = state(st) \implies  (state(st), (state \oplus  (\{(target?, nonexistent)\} \cup  \{(topReady!, running)\}))(st)) \in  transition) \implies  t \in  TASK \land  state(t) = ready \land  \lnot  priority(topReady!) \geq  priority(t))
\end{theorem}

\begin{zproof}[lDeleteTaskS\_T\_Lemma]
prove by reduce;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
apply extensionality to predicate TASK \setminus  (\{target?\} \cup  (state \inv  \limg  \{nonexistent\} \rimg )) = \{topReady!\} \cup  (TASK \setminus  (\{target?\} \cup  (state \inv  \limg  \{nonexistent\} \rimg )));
apply extensionality to predicate (state \oplus  (\{(target?, nonexistent)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{running\} \rimg  = \{topReady!\};
prove;
with enabled (applyOverride) prove;
instantiate x == target?;
cases;
with normalization prove;
next;
instantiate x\_\_0 == x;
with enabled (applyOverride) with normalization prove;
next;
split state(idle) = running;
prove;
next;
instantiate rtsk == pt;
with enabled (applyOverride) with normalization prove;
next;
split st = target?;
prove;
next;
instantiate rtsk == t;
prove;
next;
\end{zproof}

\begin{theorem}{DeleteTaskS\_T\_vc\_ref}
\forall  DeleteTaskS\_TFSBSig | true @ \pre  DeleteTaskS\_T
\end{theorem}

\begin{zproof}[DeleteTaskS\_T\_vc\_ref]
use findDelegate[a := state \inv  \limg  \{ready\} \rimg, g := priority ];
with disabled (Task) prove by reduce;
instantiate running\_task' == f (state \inv  \limg  \{ready\} \rimg );
prove;
use lDeleteTaskS\_T\_Lemma[topReady! := f (state \inv  \limg  \{ready\} \rimg )];
prove;
instantiate t\_\_0 == rtsk;
prove;
\end{zproof}

\begin{zed}
DeleteTask\_T \defs DeleteTaskN\_T \lor  DeleteTaskS\_T
\end{zed}

\begin{schema}{ExecuteRunningTask\_T}
  \Delta Task\\
  target!: TASK
\where
  \Xi TaskData\\
  \Xi StateData\\
  phys\_context' \neq  phys\_context\\
  log\_context' = log\_context\\
  \Xi PrioData\\
  target! = running\_task
\end{schema}

\begin{schema}{ExecuteRunningTask\_TFSBSig}
  Task
\where
  \exists  phys\_context': CONTEXT @ phys\_context' \neq  phys\_context
\end{schema}

\begin{theorem}{ExecuteRunningTask\_T\_vc\_ref}
\forall  ExecuteRunningTask\_TFSBSig | true @ \pre  ExecuteRunningTask\_T
\end{theorem}

\begin{zproof}[ExecuteRunningTask\_T\_vc\_ref]
with disabled (TaskData, StateData, PrioData) prove by reduce;
\end{zproof}

\begin{schema}{SuspendTaskN\_T}
  \Delta Task\\
  target?: TASK\\
  topReady!: TASK
\where
  target? \in  tasks \setminus  \{idle\}\\
  state(target?) \in  \{ready, blocked\}\\
  \Xi TaskData\\
  state' = state \oplus  \{(target? \mapsto  suspended)\}\\
  \Xi ContextData\\
  \Xi PrioData\\
  topReady! = running\_task
\end{schema}

\begin{schema}{SuspendTaskN\_TFSBSig}
  Task\\
  target?: TASK
\where
  target? \in  tasks \setminus  \{idle\}\\
  state(target?) \in  \{ready, blocked\}
\end{schema}

\begin{theorem}{SuspendTaskN\_T\_vc\_ref}
\forall  SuspendTaskN\_TFSBSig | true @ \pre  SuspendTaskN\_T
\end{theorem}

\begin{zproof}[SuspendTaskN\_T\_vc\_ref]
prove by reduce;
apply extensionality to predicate TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ) = \{target?\} \cup  (TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ));
instantiate pt\_\_0 == pt;
prove;
apply applyOverride;
prove;
cases;
with normalization prove;
next;
with normalization prove;
next;
with normalization prove;
next;
with normalization prove;
next;
\end{zproof}

\begin{schema}{SuspendTaskS\_T}
  \Delta Task\\
  target?: TASK\\
  topReady!: TASK
\where
  target? \in  tasks \setminus  \{idle\}\\
  state(target?) \in  \{running\}\\
  state(topReady!) = ready\\
  \forall  t: state \inv  \limg  \{ready\} \rimg  @ priority(topReady!) \geq  priority(t)\\
  \exists  st?: STATE | st? = suspended @ Reschedule[tasks/tasks?, priority/pri?, topReady!/target?]
\end{schema}

\begin{theorem}{TaskProperty4}
\forall  Task | SuspendTaskS\_T @ state'(running\_task) = suspended \land  (\forall  t: state \inv  \limg  \{ready\} \rimg  @ priority(running\_task') \geq  priority(t))
\end{theorem}

\begin{zproof}[TaskProperty4]
with disabled (\Delta Task, Task) prove by reduce;
use TaskProperty3[t := topReady!];
instantiate t\_\_0 == t;
prove;
\end{zproof}

\begin{theorem}{TaskProperty5}
\forall  Task @ \forall  t: TASK | t \notin  tasks @ state(t) = nonexistent
\end{theorem}

\begin{zproof}[TaskProperty5]
prove by reduce;
\end{zproof}

\begin{schema}{SuspendTaskS\_TFSBSig}
  Task\\
  target?: TASK
\where
  target? \in  tasks \setminus  \{idle\}\\
  state(target?) \in  \{running\}
\end{schema}

\begin{theorem}{lSuspendTaskS\_T\_Lemma}
\forall  Task; target?, topReady!: TASK | target? \in  tasks \setminus  \{idle\} \land  state(target?) \in  \{running\} \land  state(topReady!) = ready \land  (\forall  rtsk: state \inv  \limg  \{ready\} \rimg  @ priority(topReady!) \geq  priority(rtsk)) @ \lnot  (Task[log\_context := log\_context \oplus  \{(running\_task, phys\_context)\}, phys\_context := log\_context(topReady!), running\_task := topReady!, state := state \oplus  (\{(running\_task, suspended)\} \cup  \{(topReady!, running)\})] \land  (st \in  TASK \land  \lnot  (state \oplus  (\{(running\_task, suspended)\} \cup  \{(topReady!, running)\})) st = state(st) \implies  (state(st), (state \oplus  (\{(running\_task, suspended)\} \cup  \{(topReady!, running)\})) st) \in  transition) \implies  t \in  TASK \land  state(t) = ready \land  \lnot  priority(topReady!) \geq  priority(t))
\end{theorem}

\begin{zproof}[lSuspendTaskS\_T\_Lemma]
prove by reduce;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
apply extensionality to predicate TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ) = TASK \setminus  ((state \oplus  (\{(running\_task, suspended)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{nonexistent\} \rimg );
apply extensionality to predicate (state \oplus  (\{(running\_task, suspended)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{running\} \rimg  = \{topReady!\};
prove;
with enabled (applyOverride) prove;
instantiate x == target?;
cases;
with normalization prove;
next;
instantiate x\_\_0 == x;
with enabled (applyOverride) with normalization prove;
next;
with normalization prove;
next;
instantiate rtsk == pt;
with normalization prove;
next;
split st = running\_task;
prove;
next;
instantiate rtsk == t;
prove;
next;
\end{zproof}

\begin{theorem}{SuspendTaskS\_T\_vc\_ref}
\forall  SuspendTaskS\_TFSBSig | true @ \pre  SuspendTaskS\_T
\end{theorem}

\begin{zproof}[SuspendTaskS\_T\_vc\_ref]
use findDelegate[a := state \inv  \limg  \{ready\} \rimg, g := priority ];
with disabled (Task) prove by reduce;
instantiate running\_task' == f (state \inv  \limg  \{ready\} \rimg );
prove;
use lSuspendTaskS\_T\_Lemma[topReady! := f (state \inv  \limg  \{ready\} \rimg )];
prove;
instantiate t\_\_0 == rtsk;
prove;
\end{zproof}

\begin{schema}{SuspendTaskO\_T}
  \Xi Task\\
  target?: TASK\\
  topReady!: TASK
\where
  state(target?) \in  \{suspended\}\\
  topReady! = running\_task
\end{schema}

\begin{schema}{SuspendTaskO\_TFSBSig}
  Task\\
  target?: TASK\\
  topReady!: TASK
\where
  state(target?) \in  \{suspended\}
\end{schema}

\begin{theorem}{SuspendTaskO\_T\_vc\_ref}
\forall  SuspendTaskO\_TFSBSig | true @ \pre  SuspendTaskO\_T
\end{theorem}

\begin{zproof}[SuspendTaskO\_T\_vc\_ref]
prove by reduce;
\end{zproof}

\begin{zed}
SuspendTask\_T \defs SuspendTaskN\_T \lor  SuspendTaskS\_T \lor  SuspendTaskO\_T
\end{zed}

\begin{schema}{ResumeTaskN\_T}
  \Delta Task\\
  target?: TASK
\where
  state(target?) = suspended\\
  priority(target?) \leq  priority(running\_task)\\
  \Xi TaskData\\
  state' = state \oplus  \{(target? \mapsto  ready)\}\\
  \Xi ContextData\\
  \Xi PrioData
\end{schema}

\begin{schema}{ResumeTaskN\_TFSBSig}
  Task\\
  target?: TASK
\where
  state(target?) = suspended\\
  priority(target?) \leq  priority(running\_task)
\end{schema}

\begin{theorem}{ResumeTaskN\_T\_vc\_ref}
\forall  ResumeTaskN\_TFSBSig | true @ \pre  ResumeTaskN\_T
\end{theorem}

\begin{zproof}[ResumeTaskN\_T\_vc\_ref]
prove by reduce;
apply extensionality to predicate TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ) = \{target?\} \cup  (TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ));
with enabled (applyOverride) prove;
apply applyOverride;
instantiate pt\_\_0 == pt;
with normalization prove;
\end{zproof}

\begin{schema}{ResumeTaskS\_T}
  \Delta Task\\
  target?: TASK
\where
  state(target?) = suspended\\
  priority(target?) > priority(running\_task)\\
  \exists  st?: STATE | st? = ready @ Reschedule[tasks/tasks?, priority/pri?]
\end{schema}

\begin{schema}{ResumeTaskS\_TFSBSig}
  Task\\
  target?: TASK
\where
  state(target?) = suspended\\
  priority(target?) > priority(running\_task)
\end{schema}

\begin{theorem}{ResumeTaskS\_T\_vc\_ref}
\forall  ResumeTaskS\_TFSBSig | true @ \pre  ResumeTaskS\_T
\end{theorem}

\begin{zproof}[ResumeTaskS\_T\_vc\_ref]
prove by reduce;
apply extensionality to predicate \{target?\} \cup  (TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ) \cup  (state \inv  \limg  \{running\} \rimg )) = TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg );
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
apply extensionality to predicate (state \oplus  (\{(running\_task, ready)\} \cup  \{(target?, running)\})) \inv  \limg  \{running\} \rimg  = \{target?\};
prove;
apply applyOverride;
instantiate x\_\_1 == x\_\_0;
instantiate pt\_\_0 == pt;
cases;
with normalization prove;
next;
with normalization prove;
next;
with normalization prove;
next;
with normalization prove;
next;
with normalization prove;
next;
with normalization prove;
next;
\end{zproof}

\begin{zed}
ResumeTask\_T \defs ResumeTaskN\_T \lor  ResumeTaskS\_T
\end{zed}

\begin{schema}{ChangeTaskPriorityN\_T}
  \Delta Task\\
  newpri?: \nat \\
  target?: TASK\\
  topReady!: TASK
\where
  state(target?) = ready \implies  newpri? \leq  priority(running\_task)\\
  state(target?) = running \implies  (\forall  t: state \inv  \limg  \{ready\} \rimg  @ newpri? \geq  priority(t))\\
  state(target?) \neq  nonexistent\\
  target? = idle \implies  newpri? = 0\\
  \Xi TaskData\\
  \Xi StateData\\
  \Xi ContextData\\
  priority' = priority \oplus  \{(target? \mapsto  newpri?)\}\\
  topReady! = running\_task
\end{schema}

\begin{schema}{ChangeTaskPriorityN\_TFSBSig}
  Task\\
  newpri?: \nat \\
  target?: TASK
\where
  state(target?) = ready \implies  newpri? \leq  priority(running\_task)\\
  state(target?) = running \implies  (\forall  t: state \inv  \limg  \{ready\} \rimg  @ newpri? \geq  priority(t))\\
  state(target?) \neq  nonexistent\\
  target? = idle \implies  newpri? = 0
\end{schema}

\begin{theorem}{ChangeTaskPriorityN\_T\_vc\_ref}
\forall  ChangeTaskPriorityN\_TFSBSig | true @ \pre  ChangeTaskPriorityN\_T
\end{theorem}

\begin{zproof}[ChangeTaskPriorityN\_T\_vc\_ref]
with enabled (applyOverride) prove by reduce;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
instantiate t == pt;
with normalization prove;
\end{zproof}

\begin{schema}{ChangeTaskPriorityS\_T}
  \Delta Task\\
  target?: TASK\\
  newpri?: \nat \\
  topReady!: TASK
\where
  state(target?) = ready\\
  newpri? > priority(running\_task)\\
  target? = idle \implies  newpri? = 0\\
  \exists  st?: STATE; pri?: TASK \fun  \nat  | st? = ready \land  pri? = priority \oplus  \{(target? \mapsto  newpri?)\} @ Reschedule[tasks/tasks?]\\
  topReady! = target?
\end{schema}

\begin{schema}{ChangeTaskPriorityS\_TFSBSig}
  Task\\
  newpri?: \nat \\
  target?: TASK
\where
  state(target?) = ready\\
  newpri? > priority(running\_task)\\
  target? = idle \implies  newpri? = 0
\end{schema}

\begin{theorem}{ChangeTaskPriorityS\_T\_vc\_ref}
\forall  ChangeTaskPriorityS\_TFSBSig | true @ \pre  ChangeTaskPriorityS\_T
\end{theorem}

\begin{zproof}[ChangeTaskPriorityS\_T\_vc\_ref]
prove by reduce;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
apply extensionality to predicate TASK \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(target?, running)\})) \inv  \limg  \{nonexistent\} \rimg ) = TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg );
apply extensionality to predicate (state \oplus  (\{(running\_task, ready)\} \cup  \{(target?, running)\})) \inv  \limg  \{running\} \rimg  = \{target?\};
prove;
with enabled (applyOverride) prove;
apply applyOverride;
apply applyCupRight;
apply applyCupLeft;
prove;
instantiate x\_\_1 == x\_\_0;
instantiate pt\_\_0 == pt;
cases;
with normalization reduce;
next;
with normalization reduce;
next;
with normalization reduce;
next;
with normalization reduce;
next;
\end{zproof}

\begin{schema}{ChangeTaskPriorityD\_T}
  \Delta Task\\
  target?: TASK\\
  topReady!: TASK\\
  newpri?: \nat 
\where
  state(target?) = running\\
  target? = idle \implies  newpri? = 0\\
  state(topReady!) = ready\\
  \forall  t: state \inv  \limg  \{ready\} \rimg  @ priority(topReady!) \geq  priority(t)\\
  newpri? < priority(topReady!)\\
  \exists  st?: STATE; pri?: TASK \fun  \nat  | st? = ready \land  pri? = priority \oplus  \{(target? \mapsto  newpri?)\} @ Reschedule[tasks/tasks?, topReady!/target?]
\end{schema}

\begin{schema}{ChangeTaskPriorityD\_TFSBSig}
  Task\\
  newpri?: \nat \\
  target?: TASK
\where
  state(target?) = running\\
  target? = idle \implies  newpri? = 0\\
  \exists  readyTask: state \inv  \limg  \{ready\} \rimg  @ newpri? < priority(readyTask)
\end{schema}

\begin{theorem}{lChangeTaskPriorityD\_T\_Lemma}
\forall  Task; target?, topReady!: TASK; newpri?: \nat  | state(target?) = running \land  (target? = idle \implies  newpri? = 0) \land  state(topReady!) = ready \land  (\forall  rtsk: state \inv  \limg  \{ready\} \rimg  @ priority(topReady!) \geq  priority(rtsk)) \land  newpri? < priority(topReady!) @ \lnot  (Task[log\_context := log\_context \oplus  \{(running\_task, phys\_context)\}, phys\_context := log\_context(topReady!), priority := priority \oplus  \{(target?, newpri?)\}, running\_task := topReady!, state := state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})] \land  (st \in  TASK \land  \lnot  (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) st = state(st) \implies  (state(st), (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) st) \in  transition) \implies  t \in  TASK \land  state(t) = ready \land  \lnot  priority(topReady!) \geq  priority(t))
\end{theorem}

\begin{zproof}[lChangeTaskPriorityD\_T\_Lemma]
prove by reduce;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
apply extensionality to predicate TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ) = TASK \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{nonexistent\} \rimg );
apply extensionality to predicate (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{running\} \rimg  = \{topReady!\};
prove;
with enabled (applyOverride) prove;
instantiate x == target?;
cases;
with normalization reduce;
next;
instantiate x\_\_0 == x;
with enabled (applyOverride) with normalization prove;
next;
with normalization reduce;
next;
instantiate rtsk == pt;
with normalization reduce;
next;
with normalization reduce;
next;
instantiate rtsk == t;
prove;
next;
\end{zproof}

\begin{theorem}{ChangeTaskPriorityD\_T\_vc\_ref}
\forall  ChangeTaskPriorityD\_TFSBSig | true @ \pre  ChangeTaskPriorityD\_T
\end{theorem}

\begin{zproof}[ChangeTaskPriorityD\_T\_vc\_ref]
use findDelegate[a := state \inv  \limg  \{ready\} \rimg, g := priority ];
with disabled (Task) prove by reduce;
instantiate running\_task' == f (state \inv  \limg  \{ready\} \rimg );
prove;
use lChangeTaskPriorityD\_T\_Lemma[topReady! := f (state \inv  \limg  \{ready\} \rimg )];
prove;
instantiate t\_\_0 == readyTask;
instantiate t\_\_0 == rtsk;
instantiate t\_\_0 == t;
prove;
\end{zproof}

\begin{zed}
ChangeTaskPriority\_T \defs ChangeTaskPriorityN\_T \lor  ChangeTaskPriorityS\_T \lor  ChangeTaskPriorityD\_T
\end{zed}

\begin{theorem}{CaseStudyStep1}
\forall  Task; target?: TASK; newpri?: \nat  | tasks = \{idle\} \land  running\_task = idle \land  newpri? = 1 \land  CreateTask\_T @ target? \in  tasks' \land  state'(target?) = running \land  priority'(target?) = 1
\end{theorem}

\begin{zproof}[CaseStudyStep1]
with disabled (CreateTaskS\_T, StateData, TaskData, ContextData) reduce;
prove by reduce;
\end{zproof}

\begin{theorem}{CaseStudyStep3}
\forall  Task; target?: TASK; newpri?: \nat  | tasks = \{idle, Task1, Task2\} \land  priority(Task1) = 1 \land  priority(Task2) = 2 \land  state(Task1) = ready \land  running\_task = Task2 \land  target? = Task1 \land  newpri? = 3 \land  ChangeTaskPriority\_T @ priority'(Task1) = 3 \land  running\_task' = Task1
\end{theorem}

\begin{zproof}[CaseStudyStep3]
with disabled (Task, ChangeTaskPriorityS\_T) prove by reduce;
prove by reduce;
\end{zproof}

\begin{theorem}{CaseStudyStep5}
\forall  Task; Task1, Task2, Task3, target?: TASK | tasks = \{idle, Task1, Task2, Task3\} \land  priority(Task1) = 3 \land  priority(Task2) = 2 \land  priority(Task3) = 4 \land  state(Task1) = ready \land  state(Task2) = ready \land  state(Task3) = running \land  target? = Task3 \land  DeleteTask\_T @ state'(Task3) = nonexistent \land  Task3 \notin  tasks' \land  running\_task' = Task1
\end{theorem}

\begin{zproof}[CaseStudyStep5]
with disabled (Task, DeleteTaskS\_T) reduce;
invoke Task;
invoke DeleteTaskS\_T;
apply extensionality to predicate tasks = TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg );
instantiate y == topReady!;
instantiate t == Task1;
invoke PrioData;
split topReady! = idle;
prove;
\end{zproof}

\begin{zed}
  [QUEUE]
\end{zed}

\begin{schema}{QueueData}
  queue: \power  QUEUE\\
  q\_max: QUEUE \pfun  \nat _1{}\\
  q\_size: QUEUE \pfun  \nat 
\where
  \dom  q\_max = \dom  q\_size\\
  \dom  q\_size = queue\\
  \forall  q: QUEUE | q \in  queue @ q\_size(q) \leq  q\_max(q)
\end{schema}

\begin{zproof}[QueueData\$domainCheck]
prove;
\end{zproof}

\begin{schema}{Init\_QueueData}
  QueueData~'
\where
  queue' = \emptyset\\
  q\_max' = \emptyset\\
  q\_size' = \emptyset
\end{schema}

\begin{theorem}{QueueDataInit}
\exists  QueueData~' @ Init\_QueueData
\end{theorem}

\begin{zproof}[QueueDataInit]
prove by reduce;
\end{zproof}

\begin{schema}{WaitingData}
  wait\_snd: TASK \pfun  QUEUE\\
  wait\_rcv: TASK \pfun  QUEUE
\where
  \dom  wait\_snd \cap  \dom  wait\_rcv = \emptyset
\end{schema}

\begin{schema}{Init\_WaitingData}
  WaitingData~'
\where
  wait\_snd' = \emptyset\\
  wait\_rcv' = \emptyset
\end{schema}

\begin{theorem}{WaitingDataInit}
\exists  WaitingData~' @ Init\_WaitingData
\end{theorem}

\begin{zproof}[WaitingDataInit]
prove by reduce;
\end{zproof}

\begin{schema}{QReleasingData}
  release\_snd: TASK \pfun  QUEUE\\
  release\_rcv: TASK \pfun  QUEUE
\where
  \dom  release\_snd \cap  \dom  release\_rcv = \emptyset
\end{schema}

\begin{schema}{Init\_QReleasingData}
  QReleasingData~'
\where
  release\_snd' = \emptyset\\
  release\_rcv' = \emptyset
\end{schema}

\begin{theorem}{QReleasingDataInit}
\exists  QReleasingData~' @ Init\_QReleasingData
\end{theorem}

\begin{zproof}[QReleasingDataInit]
prove by reduce;
\end{zproof}

\begin{schema}{Queue}
  QueueData\\
  WaitingData\\
  QReleasingData
\where
  \ran  wait\_snd \subseteq  queue\\
  \ran  wait\_rcv \subseteq  queue\\
  \ran  release\_snd \subseteq  queue\\
  \ran  release\_rcv \subseteq  queue\\
  (\dom  wait\_snd \cup  \dom  wait\_rcv) \cap  (\dom  release\_snd \cup  \dom  release\_rcv) = \emptyset
\end{schema}

\begin{theorem}{QueueProperty1}
\forall  Queue @ \forall  q: queue @ q\_max(q) > 0
\end{theorem}

\begin{zproof}[QueueProperty1]
prove by reduce;
use applyInRanPfun[QUEUE, \num ][A := QUEUE, B := \nat _1{}, f := q\_max, a := q];
prove;
\end{zproof}

\begin{theorem}{ImageProperty1}
\forall  f: TASK \pfun  QUEUE @ \forall  y: QUEUE @ f \inv  \limg  \{y\} \rimg  \neq  \emptyset \iff  y \in  \ran  f
\end{theorem}

\begin{zproof}[ImageProperty1]
prove;
apply extensionality to predicate f \inv  \limg  \{y\} \rimg  = \{\};
apply inRanFunction to predicate y \in  \ran  f;
cases;
prove;
instantiate x\_\_0 == x;
prove;
next;
prove;
instantiate x\_\_0 == x;
prove;
next;
\end{zproof}

\begin{schema}{Init\_Queue}
  Queue~'
\where
  Init\_QueueData\\
  Init\_WaitingData\\
  Init\_QReleasingData
\end{schema}

\begin{theorem}{QueueInit}
\exists  Queue~' @ Init\_Queue
\end{theorem}

\begin{zproof}[QueueInit]
prove by reduce;
\end{zproof}

\begin{schema}{TaskQueue}
  Task\\
  Queue
\where
  \dom  wait\_snd \subseteq  state \inv  \limg  \{blocked\} \rimg \\
  \dom  wait\_rcv \subseteq  state \inv  \limg  \{blocked\} \rimg 
\end{schema}

\begin{schema}{Init\_TaskQueue}
  TaskQueue~'
\where
  Init\_Task\\
  Init\_Queue
\end{schema}

\begin{theorem}{TaskQueueInit}
\exists  TaskQueue~' @ Init\_TaskQueue
\end{theorem}

\begin{zproof}[TaskQueueInit]
use TaskInit;
prove by reduce;
\end{zproof}

\begin{zed}
\Delta TaskQueue \defs TaskQueue \land  TaskQueue~' \land  \Delta Task
\end{zed}

\begin{schema}{ExtendTaskXi}
  \Delta TaskQueue
\where
  running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv\\
  \Xi Queue
\end{schema}

\begin{schema}{ExtTaskFSBSig}
  TaskQueue
\where
  running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv
\end{schema}

\begin{zed}
CreateTaskN\_TQ \defs ExtendTaskXi \land  CreateTaskN\_T
\end{zed}

\begin{zed}
CreateTaskN\_TQFSBSig \defs ExtTaskFSBSig \land  CreateTaskN\_TFSBSig
\end{zed}

\begin{theorem}{CreateTaskN\_TQ\_vc\_ref}
\forall  CreateTaskN\_TQFSBSig | true @ \pre  CreateTaskN\_TQ
\end{theorem}

\begin{zproof}[CreateTaskN\_TQ\_vc\_ref]
use CreateTaskN\_T\_vc\_ref;
prove by reduce;
instantiate st\_\_0 == st;
prove;
apply inPower;
prove;
instantiate e\_\_5 == e;
instantiate e\_\_6 == e\_\_0;
apply applyOverride;
prove;
split pt \in  TASK;
prove;
instantiate pt\_\_1 == pt;
prove;
\end{zproof}

\begin{zed}
CreateTaskS\_TQ \defs ExtendTaskXi \land  CreateTaskS\_T
\end{zed}

\begin{zed}
CreateTaskS\_TQFSBSig \defs ExtTaskFSBSig \land  CreateTaskS\_TFSBSig
\end{zed}

\begin{theorem}{CreateTaskS\_TQ\_vc\_ref}
\forall  CreateTaskS\_TQFSBSig | true @ \pre  CreateTaskS\_TQ
\end{theorem}

\begin{zproof}[CreateTaskS\_TQ\_vc\_ref]
use CreateTaskS\_T\_vc\_ref;
prove by reduce;
instantiate st\_\_0 == st;
prove;
apply inPower;
prove;
instantiate e\_\_5 == e;
instantiate e\_\_6 == e\_\_0;
apply applyOverride;
prove;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
cases;
prove;
next;
prove;
next;
instantiate pt\_\_0 == pt;
split state(pt) = ready;
prove;
next;
\end{zproof}

\begin{zed}
CreateTask\_TQ \defs CreateTaskN\_TQ \lor  CreateTaskS\_TQ
\end{zed}

\begin{schema}{DeleteTaskN\_TQ}
  DeleteTaskN\_T\\
  \Delta TaskQueue
\where
  running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv\\
  \Xi QueueData\\
  wait\_snd' = \{target?\} \ndres  wait\_snd\\
  wait\_rcv' = \{target?\} \ndres  wait\_rcv\\
  release\_snd' = \{target?\} \ndres  release\_snd\\
  release\_rcv' = \{target?\} \ndres  release\_rcv
\end{schema}

\begin{zed}
DeleteTaskN\_TQFSBSig \defs ExtTaskFSBSig \land  DeleteTaskN\_TFSBSig
\end{zed}

\begin{theorem}{DeleteTaskN\_TQ\_vc\_ref}
\forall  DeleteTaskN\_TQFSBSig | true @ \pre  DeleteTaskN\_TQ
\end{theorem}

\begin{zproof}[DeleteTaskN\_TQ\_vc\_ref]
use DeleteTaskN\_T\_vc\_ref;
prove by reduce;
instantiate st\_\_0 == st;
prove;
apply extensionality to predicate (\dom  wait\_rcv \setminus  \{target?\}) \cap  (\dom  wait\_snd \setminus  \{target?\}) = \{\};
apply extensionality to predicate (\dom  release\_rcv \setminus  \{target?\}) \cap  (\dom  release\_snd \setminus  \{target?\}) = \{\};
apply extensionality to predicate (\dom  release\_rcv \setminus  \{target?\} \cup  (\dom  release\_snd \setminus  \{target?\})) \cap  (\dom  wait\_rcv \setminus  \{target?\} \cup  (\dom  wait\_snd \setminus  \{target?\})) = \{\};
prove;
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
apply extensionality to predicate \dom  release\_rcv \cap  \dom  release\_snd = \{\};
apply extensionality to predicate (\dom  release\_rcv \cup  \dom  release\_snd) \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
instantiate x\_\_2 == x;
instantiate x\_\_3 == x\_\_0;
instantiate x\_\_4 == x\_\_1;
prove;
apply inPower;
prove;
instantiate e\_\_5 == e;
instantiate e\_\_6 == e\_\_0;
instantiate e\_\_7 == e\_\_1;
instantiate e\_\_8 == e\_\_2;
instantiate e\_\_9 == e\_\_3;
instantiate e\_\_10 == e\_\_4;
apply inRan;
prove;
instantiate x\_\_9 == x\_\_2;
instantiate x\_\_10 == x\_\_3;
instantiate x\_\_11 == x\_\_4;
instantiate x\_\_12 == x\_\_5;
apply applyOverride;
instantiate pt\_\_0 == pt;
split x\_\_5 = target?;
prove;
\end{zproof}

\begin{zed}
DeleteTaskS\_TQ \defs ExtendTaskXi \land  DeleteTaskS\_T
\end{zed}

\begin{zed}
DeleteTaskS\_TQFSBSig \defs ExtTaskFSBSig \land  DeleteTaskS\_TFSBSig
\end{zed}

\begin{theorem}{lDeleteTaskS\_TQ\_Lemma}
\forall  TaskQueue; topReady!, target?: TASK | running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv \land  target? \in  tasks \setminus  \{idle\} \land  state(target?) \in  \{running\} \land  state(topReady!) = ready \land  (\forall  rtsk: state \inv  \limg  \{ready\} \rimg  @ priority(topReady!) \geq  priority(rtsk)) @ \lnot  (TaskQueue[log\_context := log\_context \oplus  \{(target?, bare\_context)\}, phys\_context := log\_context(topReady!), running\_task := topReady!, state := state \oplus  (\{(target?, nonexistent)\} \cup  \{(topReady!, running)\}), tasks := tasks \setminus  \{target?\}] \land  (st \in  TASK \land  \lnot  (state \oplus  (\{(target?, nonexistent)\} \cup  \{(topReady!, running)\})) st = state(st) \implies  (state(st), (state \oplus  (\{(target?, nonexistent)\} \cup  \{(topReady!, running)\})) st) \in  transition) \implies  t \in  TASK \land  state(t) = ready \land  \lnot  priority(topReady!) \geq  priority(t))
\end{theorem}

\begin{zproof}[lDeleteTaskS\_TQ\_Lemma]
with disabled (Task) prove by reduce;
use lDeleteTaskS\_T\_Lemma;
prove;
instantiate rtsk\_\_0 == rtsk;
prove by reduce;
apply inPower;
prove;
instantiate e\_\_5 == e;
instantiate e\_\_6 == e\_\_0;
apply applyOverride;
cases;
prove;
next;
prove;
next;
instantiate rtsk\_\_0 == t;
prove;
next;
\end{zproof}

\begin{theorem}{DeleteTaskS\_TQ\_vc\_ref}
\forall  DeleteTaskS\_TQFSBSig | true @ \pre  DeleteTaskS\_TQ
\end{theorem}

\begin{zproof}[DeleteTaskS\_TQ\_vc\_ref]
use findDelegate[a := state \inv  \limg  \{ready\} \rimg, g := priority ];
with disabled (TaskQueue) prove by reduce;
instantiate running\_task' == f (state \inv  \limg  \{ready\} \rimg );
prove;
use lDeleteTaskS\_TQ\_Lemma[topReady! := f (state \inv  \limg  \{ready\} \rimg )];
prove;
instantiate t\_\_0 == rtsk;
prove;
\end{zproof}

\begin{zed}
DeleteTask\_TQ \defs DeleteTaskN\_TQ \lor  DeleteTaskS\_TQ
\end{zed}

\begin{zed}
ExecuteRunningTask\_TQ \defs ExtendTaskXi \land  ExecuteRunningTask\_T
\end{zed}

\begin{zed}
ExecuteRunningTask\_TQFSBSig \defs ExtTaskFSBSig \land  ExecuteRunningTask\_TFSBSig
\end{zed}

\begin{theorem}{ExecuteRunningTask\_TQ\_vc\_ref}
\forall  ExecuteRunningTask\_TQFSBSig | true @ \pre  ExecuteRunningTask\_TQ
\end{theorem}

\begin{zproof}[ExecuteRunningTask\_TQ\_vc\_ref]
with disabled (TaskData, StateData, PrioData) prove by reduce;
\end{zproof}

\begin{schema}{SuspendTaskN\_TQ}
  SuspendTaskN\_T\\
  \Delta TaskQueue
\where
  running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv\\
  \Xi QueueData\\
  wait\_snd' = \{target?\} \ndres  wait\_snd\\
  wait\_rcv' = \{target?\} \ndres  wait\_rcv\\
  \Xi QReleasingData
\end{schema}

\begin{zed}
SuspendTaskN\_TQFSBSig \defs ExtTaskFSBSig \land  SuspendTaskN\_TFSBSig
\end{zed}

\begin{theorem}{SuspendTaskN\_TQ\_vc\_ref}
\forall  SuspendTaskN\_TQFSBSig | true @ \pre  SuspendTaskN\_TQ
\end{theorem}

\begin{zproof}[SuspendTaskN\_TQ\_vc\_ref]
use SuspendTaskN\_T\_vc\_ref;
prove by reduce;
apply extensionality to predicate (\dom  wait\_rcv \setminus  \{target?\}) \cap  (\dom  wait\_snd \setminus  \{target?\}) = \{\};
apply extensionality to predicate (\dom  release\_rcv \cup  \dom  release\_snd) \cap  (\dom  wait\_rcv \setminus  \{target?\} \cup  (\dom  wait\_snd \setminus  \{target?\})) = \{\};
prove;
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
apply extensionality to predicate (\dom  release\_rcv \cup  \dom  release\_snd) \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
instantiate x\_\_1 == x;
instantiate x\_\_2 == x\_\_0;
apply inPower;
prove;
instantiate e\_\_3 == e;
instantiate e\_\_4 == e\_\_0;
instantiate e\_\_7 == e\_\_1;
instantiate e\_\_8 == e\_\_2;
with enabled (inRan) prove;
instantiate x\_\_5 == x\_\_1;
instantiate x\_\_6 == x\_\_2;
apply applyOverride;
instantiate pt\_\_0 == pt;
prove;
\end{zproof}

\begin{zed}
SuspendTaskS\_TQ \defs ExtendTaskXi \land  SuspendTaskS\_T
\end{zed}

\begin{zed}
SuspendTaskS\_TQFSBSig \defs ExtTaskFSBSig \land  SuspendTaskS\_TFSBSig
\end{zed}

\begin{theorem}{lSuspendTaskS\_TQ\_Lemma}
\forall  TaskQueue; target?, topReady!: TASK | running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv \land  target? \in  tasks \setminus  \{idle\} \land  state(target?) \in  \{running\} \land  state(topReady!) = ready \land  (\forall  rtsk: state \inv  \limg  \{ready\} \rimg  @ priority(topReady!) \geq  priority(rtsk)) @ \lnot  (TaskQueue[log\_context := log\_context \oplus  \{(running\_task, phys\_context)\}, phys\_context := log\_context(topReady!), running\_task := topReady!, state := state \oplus  (\{(running\_task, suspended)\} \cup  \{(topReady!, running)\})] \land  (st \in  TASK \land  \lnot  (state \oplus  (\{(running\_task, suspended)\} \cup  \{(topReady!, running)\})) st = state(st) \implies  (state(st), (state \oplus  (\{(running\_task, suspended)\} \cup  \{(topReady!, running)\})) st) \in  transition) \implies  t \in  TASK \land  state(t) = ready \land  \lnot  priority(topReady!) \geq  priority(t))
\end{theorem}

\begin{zproof}[lSuspendTaskS\_TQ\_Lemma]
use lSuspendTaskS\_T\_Lemma;
prove by reduce;
instantiate rtsk\_\_0 == rtsk;
prove;
apply inPower;
prove;
instantiate e\_\_5 == e;
instantiate e\_\_6 == e\_\_0;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
prove;
instantiate rtsk\_\_0 == pt;
apply applyOverride;
prove;
instantiate rtsk\_\_0 == t;
split pt = topReady!;
prove;
\end{zproof}

\begin{theorem}{SuspendTaskS\_TQ\_vc\_ref}
\forall  SuspendTaskS\_TQFSBSig | true @ \pre  SuspendTaskS\_TQ
\end{theorem}

\begin{zproof}[SuspendTaskS\_TQ\_vc\_ref]
use findDelegate[a := state \inv  \limg  \{ready\} \rimg, g := priority ];
with disabled (TaskQueue) prove by reduce;
instantiate running\_task' == f (state \inv  \limg  \{ready\} \rimg );
prove;
use lSuspendTaskS\_TQ\_Lemma[topReady! := f (state \inv  \limg  \{ready\} \rimg )];
prove;
instantiate t\_\_0 == rtsk;
prove;
\end{zproof}

\begin{zed}
SuspendTaskO\_TQ \defs ExtendTaskXi \land  SuspendTaskO\_T
\end{zed}

\begin{zed}
SuspendTaskO\_TQFSBSig \defs ExtTaskFSBSig \land  SuspendTaskO\_TFSBSig
\end{zed}

\begin{theorem}{SuspendTaskO\_TQ\_vc\_ref}
\forall  SuspendTaskO\_TQFSBSig | true @ \pre  SuspendTaskO\_TQ
\end{theorem}

\begin{zproof}[SuspendTaskO\_TQ\_vc\_ref]
prove by reduce;
\end{zproof}

\begin{zed}
SuspendTask\_TQ \defs SuspendTaskN\_TQ \lor  SuspendTaskS\_TQ \lor  SuspendTaskO\_TQ
\end{zed}

\begin{zed}
ResumeTaskN\_TQ \defs ExtendTaskXi \land  ResumeTaskN\_T
\end{zed}

\begin{zed}
ResumeTaskN\_TQFSBSig \defs ExtTaskFSBSig \land  ResumeTaskN\_TFSBSig
\end{zed}

\begin{theorem}{ResumeTaskN\_TQ\_vc\_ref}
\forall  ResumeTaskN\_TQFSBSig | true @ \pre  ResumeTaskN\_TQ
\end{theorem}

\begin{zproof}[ResumeTaskN\_TQ\_vc\_ref]
use ResumeTaskN\_T\_vc\_ref;
prove by reduce;
apply inPower;
prove;
instantiate e\_\_5 == e;
instantiate e\_\_6 == e\_\_0;
apply applyOverride;
prove;
instantiate pt\_\_0 == pt;
split pt = target?;
prove;
\end{zproof}

\begin{zed}
ResumeTaskS\_TQ \defs ExtendTaskXi \land  ResumeTaskS\_T
\end{zed}

\begin{zed}
ResumeTaskS\_TQFSBSig \defs ExtTaskFSBSig \land  ResumeTaskS\_TFSBSig
\end{zed}

\begin{theorem}{ResumeTaskS\_TQ\_vc\_ref}
\forall  ResumeTaskS\_TQFSBSig | true @ \pre  ResumeTaskS\_TQ
\end{theorem}

\begin{zproof}[ResumeTaskS\_TQ\_vc\_ref]
use ResumeTaskS\_T\_vc\_ref;
with disabled (runningUpdate, setminUpdate) prove by reduce;
instantiate st\_\_0 == st;
prove;
apply inPower;
prove;
instantiate e\_\_5 == e;
instantiate e\_\_6 == e\_\_0;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
prove;
apply applyOverride;
instantiate pt\_\_0 == pt;
cases;
prove;
next;
prove;
next;
split pt = running\_task;
prove;
next;
\end{zproof}

\begin{zed}
ResumeTask\_TQ \defs ResumeTaskN\_TQ \lor  ResumeTaskS\_TQ
\end{zed}

\begin{zed}
ChangeTaskPriorityN\_TQ \defs ExtendTaskXi \land  ChangeTaskPriorityN\_T
\end{zed}

\begin{zed}
ChangeTaskPriorityN\_TQFSBSig \defs ExtTaskFSBSig \land  ChangeTaskPriorityN\_TFSBSig
\end{zed}

\begin{theorem}{ChangeTaskPriorityN\_TQ\_vc\_ref}
\forall  ChangeTaskPriorityN\_TQFSBSig | true @ \pre  ChangeTaskPriorityN\_TQ
\end{theorem}

\begin{zproof}[ChangeTaskPriorityN\_TQ\_vc\_ref]
with enabled (applyOverride) prove by reduce;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
instantiate t == pt;
with normalization prove;
\end{zproof}

\begin{zed}
ChangeTaskPriorityS\_TQ \defs ExtendTaskXi \land  ChangeTaskPriorityS\_T
\end{zed}

\begin{zed}
ChangeTaskPriorityS\_TQFSBSig \defs ExtTaskFSBSig \land  ChangeTaskPriorityS\_TFSBSig
\end{zed}

\begin{theorem}{ChangeTaskPriorityS\_TQ\_vc\_ref}
\forall  ChangeTaskPriorityS\_TQFSBSig | true @ \pre  ChangeTaskPriorityS\_TQ
\end{theorem}

\begin{zproof}[ChangeTaskPriorityS\_TQ\_vc\_ref]
use ChangeTaskPriorityS\_T\_vc\_ref;
prove by reduce;
instantiate st\_\_0 == st;
instantiate pt\_\_1 == pt;
prove;
apply inPower;
prove;
instantiate e\_\_5 == e;
instantiate e\_\_6 == e\_\_0;
prove;
apply applyOverride;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
prove;
cases;
prove;
next;
prove;
next;
prove;
next;
\end{zproof}

\begin{zed}
ChangeTaskPriorityD\_TQ \defs ExtendTaskXi \land  ChangeTaskPriorityD\_T
\end{zed}

\begin{zed}
ChangeTaskPriorityD\_TQFSBSig \defs ExtTaskFSBSig \land  ChangeTaskPriorityD\_TFSBSig
\end{zed}

\begin{theorem}{lChangeTaskPriorityD\_TQ\_Lemma}
\forall  TaskQueue; target?, topReady!: TASK; newpri?: \nat  | state(target?) = running \land  (target? = idle \implies  newpri? = 0) \land  state(topReady!) = ready \land  (\forall  rtsk: state \inv  \limg  \{ready\} \rimg  @ priority(topReady!) \geq  priority(rtsk)) \land  newpri? < priority(topReady!) @ \lnot  (TaskQueue[log\_context := log\_context \oplus  \{(running\_task, phys\_context)\}, phys\_context := log\_context(topReady!), priority := priority \oplus  \{(target?, newpri?)\}, running\_task := topReady!, state := state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})] \land  newpri? < priority(topReady!) \land  (st \in  TASK \land  \lnot  (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) st = state(st) \implies  (state(st), (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) st) \in  transition) \implies  t \in  TASK \land  state(t) = ready \land  \lnot  priority(topReady!) \geq  priority(t))
\end{theorem}

\begin{zproof}[lChangeTaskPriorityD\_TQ\_Lemma]
use lChangeTaskPriorityD\_T\_Lemma;
prove by reduce;
instantiate rtsk\_\_0 == rtsk;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
prove;
apply inPower;
prove;
instantiate e\_\_5 == e;
instantiate e\_\_6 == e\_\_0;
apply applyOverride;
instantiate rtsk\_\_0 == pt;
instantiate rtsk\_\_0 == t;
prove;
cases;
prove;
next;
prove;
next;
instantiate x == target?;
prove;
next;
prove;
next;
\end{zproof}

\begin{theorem}{ChangeTaskPriorityD\_TQ\_vc\_ref}
\forall  ChangeTaskPriorityD\_TQFSBSig | true @ \pre  ChangeTaskPriorityD\_TQ
\end{theorem}

\begin{zproof}[ChangeTaskPriorityD\_TQ\_vc\_ref]
use findDelegate[a := state \inv  \limg  \{ready\} \rimg, g := priority ];
with disabled (TaskQueue) prove by reduce;
instantiate running\_task' == f (state \inv  \limg  \{ready\} \rimg );
prove;
use lChangeTaskPriorityD\_TQ\_Lemma[topReady! := f (state \inv  \limg  \{ready\} \rimg )];
prove;
instantiate t\_\_0 == readyTask;
instantiate t\_\_0 == rtsk;
instantiate t\_\_0 == t;
prove;
\end{zproof}

\begin{schema}{CreateQueue\_TQ}
  \Delta TaskQueue\\
  que?: QUEUE\\
  size?: \nat 
\where
  running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv\\
  que? \notin  queue\\
  size? > 0\\
  \Xi Task\\
  queue' = queue \cup  \{que?\}\\
  q\_max' = q\_max \oplus  \{(que? \mapsto  size?)\}\\
  q\_size' = q\_size \oplus  \{(que? \mapsto  0)\}\\
  \Xi WaitingData\\
  \Xi QReleasingData
\end{schema}

\begin{schema}{CreateQueue\_TQFSBSig}
  TaskQueue\\
  que?: QUEUE\\
  size?: \nat 
\where
  running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv\\
  que? \notin  queue\\
  size? > 0
\end{schema}

\begin{theorem}{CreateQueue\_TQ\_vc\_ref}
\forall  CreateQueue\_TQFSBSig | true @ \pre  CreateQueue\_TQ
\end{theorem}

\begin{zproof}[CreateQueue\_TQ\_vc\_ref]
prove by reduce;
apply applyOverride;
prove;
instantiate q\_\_0 == q;
apply inPower to predicate \ran  wait\_snd \in  \power  (\dom  q\_size);
instantiate e == q;
prove;
\end{zproof}

\begin{schema}{DeleteQueue\_TQ}
  \Delta TaskQueue\\
  que?: QUEUE
\where
  running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv\\
  que? \in  queue\\
  que? \notin  \ran  wait\_snd \cup  \ran  wait\_rcv\\
  que? \notin  \ran  release\_snd \cup  \ran  release\_rcv\\
  \Xi Task\\
  queue' = queue \setminus  \{que?\}\\
  q\_max' = \{que?\} \ndres  q\_max\\
  q\_size' = \{que?\} \ndres  q\_size\\
  \Xi WaitingData\\
  \Xi QReleasingData
\end{schema}

\begin{schema}{DeleteQueue\_TQFSBSig}
  TaskQueue\\
  que?: QUEUE
\where
  running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv\\
  que? \in  queue\\
  que? \notin  \ran  wait\_snd \cup  \ran  wait\_rcv\\
  que? \notin  \ran  release\_snd \cup  \ran  release\_rcv
\end{schema}

\begin{theorem}{DeleteQueue\_TQ\_vc\_ref}
\forall  DeleteQueue\_TQFSBSig | true @ \pre  DeleteQueue\_TQ
\end{theorem}

\begin{zproof}[DeleteQueue\_TQ\_vc\_ref]
prove by reduce;
apply inPower;
prove;
instantiate e\_\_3 == e;
instantiate e\_\_4 == e\_\_0;
instantiate e\_\_5 == e\_\_1;
instantiate e\_\_6 == e\_\_2;
prove;
\end{zproof}

\begin{schema}{QueueSendN\_TQ}
  \Delta TaskQueue\\
  que?: QUEUE\\
  topReady!: TASK
\where
  running\_task \notin  \dom  release\_rcv\\
  running\_task \in  \dom  release\_snd \implies  que? = release\_snd(running\_task)\\
  que? \in  queue\\
  q\_size(que?) < q\_max(que?)\\
  que? \notin  \ran  wait\_rcv\\
  \Xi Task\\
  queue' = queue\\
  q\_max' = q\_max\\
  q\_size' = q\_size \oplus  \{(que? \mapsto  q\_size(que?) + 1)\}\\
  \Xi WaitingData\\
  release\_snd' = \{running\_task\} \ndres  release\_snd\\
  release\_rcv' = release\_rcv\\
  topReady! = running\_task
\end{schema}

\begin{zproof}[QueueSendN\_TQ\$domainCheck]
prove by reduce;
\end{zproof}

\begin{schema}{QueueSendN\_TQFSBSig}
  TaskQueue\\
  que?: QUEUE
\where
  running\_task \notin  \dom  release\_rcv\\
  running\_task \in  \dom  release\_snd \implies  que? = release\_snd(running\_task)\\
  que? \in  queue\\
  q\_size(que?) < q\_max(que?)\\
  que? \notin  \ran  wait\_rcv
\end{schema}

\begin{zproof}[QueueSendN\_TQFSBSig\$domainCheck]
prove by reduce;
\end{zproof}

\begin{theorem}{QueueSendN\_TQ\_vc\_ref}
\forall  QueueSendN\_TQFSBSig | true @ \pre  QueueSendN\_TQ
\end{theorem}

\begin{zproof}[QueueSendN\_TQ\_vc\_ref]
prove by reduce;
use applyInRanPfun[QUEUE, \num ][A := QUEUE, B := \nat , f := q\_size, a := que?];
apply extensionality to predicate \dom  q\_max = \{que?\} \cup  \dom  q\_size;
apply extensionality to predicate \dom  release\_rcv \cap  (\dom  release\_snd \setminus  (state \inv  \limg  \{running\} \rimg )) = \{\};
apply extensionality to predicate \dom  release\_rcv \cap  \dom  release\_snd = \{\};
apply extensionality to predicate (\dom  release\_rcv \cup  (\dom  release\_snd \setminus  (state \inv  \limg  \{running\} \rimg ))) \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
apply extensionality to predicate (\dom  release\_rcv \cup  \dom  release\_snd) \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
with enabled (inPower) prove;
instantiate q\_\_0 == q;
instantiate x\_\_2 == x;
instantiate x\_\_3 == x\_\_0;
instantiate e\_\_2 == e;
split y = que?;
prove;
apply applyOverride;
with enabled (inRan) prove;
instantiate x\_\_6 == x\_\_2;
split state(x\_\_1) = running;
prove;
\end{zproof}

\begin{schema}{QueueSendF\_TQ}
  \Delta TaskQueue\\
  que?: QUEUE\\
  topReady!: TASK
\where
  running\_task \notin  \dom  release\_rcv\\
  running\_task \in  \dom  release\_snd \implies  que? = release\_snd(running\_task)\\
  que? \in  queue\\
  q\_size(que?) = q\_max(que?)\\
  running\_task \neq  idle\\
  state(topReady!) = ready\\
  \forall  t: state \inv  \limg  \{ready\} \rimg  @ priority(topReady!) \geq  priority(t)\\
  \exists  st?: STATE | st? = blocked @ Reschedule[topReady!/target?, tasks/tasks?, priority/pri?]\\
  \Xi QueueData\\
  wait\_snd' = wait\_snd \oplus  \{(running\_task \mapsto  que?)\}\\
  wait\_rcv' = wait\_rcv\\
  release\_snd' = \{running\_task\} \ndres  release\_snd\\
  release\_rcv' = release\_rcv
\end{schema}

\begin{zproof}[QueueSendF\_TQ\$domainCheck]
prove by reduce;
\end{zproof}

\begin{schema}{QueueSendF\_TQFSBSig}
  TaskQueue\\
  que?: QUEUE
\where
  running\_task \notin  \dom  release\_rcv\\
  running\_task \in  \dom  release\_snd \implies  que? = release\_snd(running\_task)\\
  que? \in  queue\\
  q\_size(que?) = q\_max(que?)\\
  running\_task \neq  idle
\end{schema}

\begin{zproof}[QueueSendF\_TQFSBSig\$domainCheck]
prove by reduce;
\end{zproof}

\begin{theorem}{lQueueSendF\_TQ\_Lemma}
\forall  TaskQueue; topReady!: TASK; que?: QUEUE | running\_task \notin  \dom  release\_rcv \land  (running\_task \in  \dom  release\_snd \implies  que? = release\_snd(running\_task)) \land  que? \in  queue \land  q\_size(que?) = q\_max(que?) \land  running\_task \neq  idle \land  state(topReady!) = ready \land  (\forall  rtsk: state \inv  \limg  \{ready\} \rimg  @ priority(topReady!) \geq  priority(rtsk)) @ \lnot  (TaskQueue[log\_context := log\_context \oplus  \{(running\_task, phys\_context)\}, phys\_context := log\_context(topReady!), release\_snd := \{running\_task\} \ndres  release\_snd, running\_task := topReady!, state := state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\}), wait\_snd := wait\_snd \oplus  \{(running\_task, que?)\}] \land  (t \in  TASK \land  state(t) = ready \implies  priority(topReady!) \geq  priority(t)) \implies  st \in  TASK \land  \lnot  (state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) st = state(st) \land  \lnot  (state(st), (state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) st) \in  transition)
\end{theorem}

\begin{zproof}[lQueueSendF\_TQ\_Lemma]
prove by reduce;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
apply extensionality to predicate TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ) = TASK \setminus  ((state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{nonexistent\} \rimg );
apply extensionality to predicate (state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{running\} \rimg  = \{topReady!\};
prove;
apply applyOverride;
apply inPower;
prove;
cases;
apply extensionality to predicate \dom  wait\_rcv \cap  ((state \inv  \limg  \{running\} \rimg ) \cup  \dom  wait\_snd) = \{\};
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
prove;
instantiate e\_\_4 == x;
instantiate x\_\_1 == x;
prove;
next;
apply extensionality to predicate \dom  release\_rcv \cap  (\dom  release\_snd \setminus  (state \inv  \limg  \{running\} \rimg )) = \{\};
apply extensionality to predicate \dom  release\_rcv \cap  \dom  release\_snd = \{\};
prove;
instantiate x\_\_1 == x;
prove;
next;
apply extensionality to predicate (\dom  release\_rcv \cup  (\dom  release\_snd \setminus  (state \inv  \limg  \{running\} \rimg ))) \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
apply extensionality to predicate (\dom  release\_rcv \cup  \dom  release\_snd) \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
prove;
instantiate x\_\_1 == x;
with normalization rewrite;
next;
instantiate e\_\_3 == e;
apply oplusDef to expression wait\_snd \oplus  \{(running\_task, que?)\};
with normalization prove;
with enabled (inRan) prove;
instantiate x\_\_1 == x;
prove;
next;
instantiate e\_\_5 == e\_\_0;
with enabled (inRan) prove;
instantiate x\_\_1 == x;
prove;
next;
with enabled (applyOverride) prove;
instantiate e\_\_4 == e\_\_1;
split e = running\_task;
prove;
next;
with enabled (applyOverride) prove;
instantiate e\_\_5 == e\_\_2;
split e = running\_task;
prove;
next;
with normalization rewrite;
next;
instantiate x == x\_\_0;
with normalization rewrite;
next;
prove;
next;
instantiate rtsk == pt;
split pt = running\_task;
prove;
next;
instantiate rtsk == t;
prove;
next;
with normalization rewrite;
next;
\end{zproof}

\begin{theorem}{QueueSendF\_TQ\_vc\_ref}
\forall  QueueSendF\_TQFSBSig | true @ \pre  QueueSendF\_TQ
\end{theorem}

\begin{zproof}[QueueSendF\_TQ\_vc\_ref]
use findDelegate[a := state \inv  \limg  \{ready\} \rimg, g := priority ];
with disabled (TaskQueue) prove by reduce;
instantiate running\_task' == f (state \inv  \limg  \{ready\} \rimg );
prove;
use lQueueSendF\_TQ\_Lemma[topReady! := f (state \inv  \limg  \{ready\} \rimg )];
prove;
instantiate t\_\_0 == rtsk;
prove;
with normalization rewrite;
\end{zproof}

\begin{schema}{QueueSendW\_TQ}
  \Delta TaskQueue\\
  que?: QUEUE\\
  topReady!: TASK
\where
  running\_task \notin  \dom  release\_rcv\\
  running\_task \in  \dom  release\_snd \implies  que? = release\_snd(running\_task)\\
  que? \in  queue\\
  q\_size(que?) < q\_max(que?)\\
  topReady! \in  wait\_rcv \inv  \limg  \{que?\} \rimg \\
  \forall  wr: wait\_rcv \inv  \limg  \{que?\} \rimg  @ priority(topReady!) \geq  priority(wr)\\
  priority(topReady!) \leq  priority(running\_task)\\
  \Xi TaskData\\
  state' = state \oplus  \{(topReady! \mapsto  ready)\}\\
  \Xi ContextData\\
  \Xi PrioData\\
  queue' = queue\\
  q\_max' = q\_max\\
  q\_size' = q\_size \oplus  \{(que? \mapsto  q\_size(que?) + 1)\}\\
  wait\_snd' = wait\_snd\\
  wait\_rcv' = \{topReady!\} \ndres  wait\_rcv\\
  release\_snd' = \{running\_task\} \ndres  release\_snd\\
  release\_rcv' = release\_rcv \oplus  \{(topReady! \mapsto  que?)\}
\end{schema}

\begin{zproof}[QueueSendW\_TQ\$domainCheck]
prove by reduce;
\end{zproof}

\begin{schema}{QueueSendW\_TQFSBSig}
  TaskQueue\\
  que?: QUEUE
\where
  running\_task \notin  \dom  release\_rcv\\
  running\_task \in  \dom  release\_snd \implies  que? = release\_snd(running\_task)\\
  que? \in  queue\\
  q\_size(que?) < q\_max(que?)\\
  \forall  wr: wait\_rcv \inv  \limg  \{que?\} \rimg  @ priority(running\_task) \geq  priority(wr)
\end{schema}

\begin{zproof}[QueueSendW\_TQFSBSig\$domainCheck]
prove by reduce;
\end{zproof}

\begin{theorem}{lQueueSendW\_TQ\_Lemma}
\forall  TaskQueue; que?: QUEUE; topReady!: TASK | running\_task \notin  \dom  release\_rcv \land  (running\_task \in  \dom  release\_snd \implies  que? = release\_snd(running\_task)) \land  que? \in  queue \land  q\_size(que?) < q\_max(que?) \land  topReady! \in  wait\_rcv \inv  \limg  \{que?\} \rimg  \land  (\forall  wrct: wait\_rcv \inv  \limg  \{que?\} \rimg  @ priority(topReady!) \geq  priority(wrct)) \land  priority(running\_task) \geq  priority(topReady!) @ \lnot  (TaskQueue[q\_size := q\_size \oplus  \{(que?, (1 + q\_size(que?)))\}, release\_rcv := release\_rcv \oplus  \{(topReady!, que?)\}, release\_snd := \{running\_task\} \ndres  release\_snd, state := state \oplus  \{(topReady!, ready)\}, wait\_rcv := \{topReady!\} \ndres  wait\_rcv] \land  priority(topReady!) \leq  priority(running\_task) \land  (st \in  TASK \land  \lnot  (state \oplus  \{(topReady!, ready)\}) st = state(st) \implies  (state(st), (state \oplus  \{(topReady!, ready)\}) st) \in  transition) \implies  wr \in  \dom  wait\_rcv \land  wait\_rcv(wr) = que? \land  \lnot  priority(topReady!) \geq  priority(wr))
\end{theorem}

\begin{zproof}[lQueueSendW\_TQ\_Lemma]
prove by reduce;
apply extensionality to predicate TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ) = \{topReady!\} \cup  (TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ));
apply extensionality to predicate \dom  wait\_snd \cap  (\dom  wait\_rcv \setminus  \{topReady!\}) = \{\};
prove;
apply applyOverride;
apply inPower;
prove;
instantiate e\_\_9 == topReady!;
with enabled (runningUpdate) prove;
cases;
with enabled (oplusDef) prove;
use applyInRanPfun[QUEUE, \num ][A := QUEUE, B := \nat , f := q\_size, a := wait\_rcv(topReady!)];
prove;
next;
apply extensionality to predicate \dom  q\_max = \{wait\_rcv(topReady!)\} \cup  \dom  q\_size;
with normalization prove;
next;
apply extensionality to predicate (\{topReady!\} \cup  \dom  release\_rcv) \cap  (\dom  release\_snd \setminus  (state \inv  \limg  \{running\} \rimg )) = \{\};
apply extensionality to predicate \dom  release\_rcv \cap  \dom  release\_snd = \{\};
apply extensionality to predicate (\dom  release\_rcv \cup  \dom  release\_snd) \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
prove;
instantiate x\_\_0 == x;
instantiate x\_\_1 == x;
prove;
next;
apply extensionality to predicate (\{topReady!\} \cup  (\dom  release\_rcv \cup  (\dom  release\_snd \setminus  (state \inv  \limg  \{running\} \rimg )))) \cap  (\dom  wait\_snd \cup  (\dom  wait\_rcv \setminus  \{topReady!\})) = \{\};
apply extensionality to predicate (\dom  release\_rcv \cup  \dom  release\_snd) \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
prove;
instantiate x\_\_0 == x;
instantiate x\_\_1 == x;
split x \in  \dom  wait\_snd;
prove;
next;
instantiate e\_\_5 == e;
with enabled (inRan) prove;
instantiate x\_\_0 == x;
prove;
next;
instantiate e\_\_6 == e\_\_0;
with enabled (inRan) prove;
instantiate x\_\_0 == x;
prove;
next;
instantiate e\_\_7 == e\_\_1;
apply oplusDef to expression release\_rcv \oplus  \{(topReady!, wait\_rcv(topReady!))\};
with enabled (inRan) prove;
instantiate x\_\_0 == x;
with normalization rewrite;
next;
instantiate e\_\_8 == e\_\_2;
with enabled (applyOverride) prove;
use inCap[TASK][A := \dom  wait\_snd, B := \dom  wait\_rcv, x := topReady!];
prove;
next;
instantiate e\_\_9 == e\_\_3;
prove;
next;
with normalization rewrite;
next;
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
instantiate x\_\_0 == x;
prove;
next;
instantiate pt\_\_0 == pt;
with normalization rewrite;
next;
instantiate q\_\_0 == q;
prove;
next;
invoke transition;
prove;
next;
instantiate wrct == wr;
prove;
next;
\end{zproof}

\begin{theorem}{QueueSendW\_TQ\_vc\_ref}
\forall  QueueSendW\_TQFSBSig | true @ \pre  QueueSendW\_TQ
\end{theorem}

\begin{zproof}[QueueSendW\_TQ\_vc\_ref]
use findDelegate[a := wait\_rcv \inv  \limg  \{que?\} \rimg, g := priority ];
with disabled (TaskQueue) prove by reduce;
instantiate topReady! == f (wait\_rcv \inv  \limg  \{que?\} \rimg );
prove;
use lQueueSendW\_TQ\_Lemma[topReady! := f (wait\_rcv \inv  \limg  \{que?\} \rimg )];
prove;
instantiate wr\_\_0 == f (wait\_rcv \inv  \limg  \{que?\} \rimg );
instantiate t == wrct;
with normalization rewrite;
\end{zproof}

\begin{theorem}{TaskQueueProperty1}
\forall  TaskQueue @ \forall  t: TASK | t \in  \dom  wait\_rcv @ state(t) = blocked
\end{theorem}

\begin{zproof}[TaskQueueProperty1]
prove by reduce;
apply inPower to predicate \dom  wait\_rcv \in  \power  (state \inv  \limg  \{blocked\} \rimg );
instantiate e == t;
prove;
\end{zproof}

\begin{schema}{QueueSendWS\_TQ}
  \Delta TaskQueue\\
  que?: QUEUE\\
  topReady!: TASK
\where
  running\_task \notin  \dom  release\_rcv\\
  running\_task \in  \dom  release\_snd \implies  que? = release\_snd(running\_task)\\
  que? \in  queue\\
  q\_size(que?) < q\_max(que?)\\
  topReady! \in  wait\_rcv \inv  \limg  \{que?\} \rimg \\
  \forall  wr: wait\_rcv \inv  \limg  \{que?\} \rimg  @ priority(topReady!) \geq  priority(wr)\\
  priority(topReady!) > priority(running\_task)\\
  \exists  st?: STATE | st? = ready @ Reschedule[topReady!/target?, tasks/tasks?, priority/pri?]\\
  queue' = queue\\
  q\_max' = q\_max\\
  q\_size' = q\_size \oplus  \{(que? \mapsto  q\_size(que?) + 1)\}\\
  wait\_snd' = wait\_snd\\
  wait\_rcv' = \{topReady!\} \ndres  wait\_rcv\\
  release\_snd' = \{running\_task\} \ndres  release\_snd\\
  release\_rcv' = release\_rcv \oplus  \{(topReady! \mapsto  que?)\}
\end{schema}

\begin{zproof}[QueueSendWS\_TQ\$domainCheck]
prove by reduce;
\end{zproof}

\begin{schema}{QueueSendWS\_TQFSBSig}
  TaskQueue\\
  que?: QUEUE
\where
  running\_task \notin  \dom  release\_rcv\\
  running\_task \in  \dom  release\_snd \implies  que? = release\_snd(running\_task)\\
  que? \in  queue\\
  q\_size(que?) < q\_max(que?)\\
  \exists  topReady!: wait\_rcv \inv  \limg  \{que?\} \rimg  | \forall  wr: wait\_rcv \inv  \limg  \{que?\} \rimg  @ priority(topReady!) \geq  priority(wr) @ priority(topReady!) > priority(running\_task)
\end{schema}

\begin{zproof}[QueueSendWS\_TQFSBSig\$domainCheck]
prove by reduce;
\end{zproof}

\begin{theorem}{lQueueSendWS\_TQ\_Lemma}
\forall  TaskQueue; que?: QUEUE; topReady!: TASK | running\_task \notin  \dom  release\_rcv \land  (running\_task \in  \dom  release\_snd \implies  que? = release\_snd(running\_task)) \land  que? \in  queue \land  q\_size(que?) < q\_max(que?) \land  topReady! \in  wait\_rcv \inv  \limg  \{que?\} \rimg  \land  (\forall  wrct: wait\_rcv \inv  \limg  \{que?\} \rimg  @ priority(topReady!) \geq  priority(wrct)) \land  priority(topReady!) > priority(running\_task) @ \lnot  (TaskQueue[log\_context := log\_context \oplus  \{(running\_task, phys\_context)\}, phys\_context := log\_context(topReady!), q\_size := q\_size \oplus  \{(wait\_rcv(topReady!), (1 + q\_size (wait\_rcv(topReady!))))\}, release\_rcv := release\_rcv \oplus  \{(topReady!, wait\_rcv(topReady!))\}, release\_snd := \{running\_task\} \ndres  release\_snd, running\_task := topReady!, state := state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\}), wait\_rcv := \{topReady!\} \ndres  wait\_rcv] \land  (wr \in  \dom  wait\_rcv \land  wait\_rcv(wr) = wait\_rcv(topReady!) \implies  priority(topReady!) \geq  priority(wr)) \implies  st \in  TASK \land  \lnot  (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) st = state(st) \land  \lnot  (state(st), (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) st) \in  transition)
\end{theorem}

\begin{zproof}[lQueueSendWS\_TQ\_Lemma]
prove by reduce;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
apply extensionality to predicate TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ) = \{topReady!\} \cup  (TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ) \cup  (state \inv  \limg  \{running\} \rimg ));
apply extensionality to predicate (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{running\} \rimg  = \{topReady!\};
prove;
apply applyOverride;
apply inPower;
instantiate e\_\_4 == topReady!;
prove;
cases;
apply oplusDef to expression q\_size \oplus  \{(wait\_rcv(topReady!), (1 + q\_size (wait\_rcv(topReady!))))\};
use applyInRanPfun[QUEUE, \num ][A := QUEUE, B := \nat , f := q\_size, a := wait\_rcv(topReady!)];
prove;
next;
apply extensionality to predicate \dom  q\_max = \{wait\_rcv(topReady!)\} \cup  \dom  q\_size;
with normalization prove;
next;
apply extensionality to predicate \dom  wait\_snd \cap  (\dom  wait\_rcv \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{running\} \rimg )) = \{\};
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
with enabled (applyOverride) prove;
instantiate x\_\_1 == x;
prove;
next;
apply extensionality to predicate (((state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{running\} \rimg ) \cup  \dom  release\_rcv) \cap  (\dom  release\_snd \setminus  (state \inv  \limg  \{running\} \rimg )) = \{\};
apply extensionality to predicate \dom  release\_rcv \cap  \dom  release\_snd = \{\};
apply extensionality to predicate (\dom  release\_rcv \cup  \dom  release\_snd) \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
with enabled (applyOverride) prove;
instantiate x\_\_1 == x;
instantiate x\_\_2 == x;
prove;
next;
apply extensionality to predicate (((state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{running\} \rimg ) \cup  (\dom  release\_rcv \cup  (\dom  release\_snd \setminus  (state \inv  \limg  \{running\} \rimg )))) \cap  (\dom  wait\_snd \cup  (\dom  wait\_rcv \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{running\} \rimg ))) = \{\};
apply extensionality to predicate (\dom  release\_rcv \cup  \dom  release\_snd) \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
prove;
apply applyOverride;
instantiate x\_\_0 == x;
instantiate x\_\_1 == x;
instantiate x\_\_2 == x;
with normalization rewrite;
next;
instantiate e\_\_5 == e;
with enabled (inRan) prove;
instantiate x\_\_1 == x;
prove;
next;
instantiate e\_\_6 == e\_\_0;
with enabled (inRan) prove;
instantiate x\_\_1 == x;
prove;
next;
instantiate e\_\_7 == e\_\_1;
apply oplusDef to expression release\_rcv \oplus  \{(topReady!, wait\_rcv(topReady!))\};
with enabled (inRan) prove;
instantiate x\_\_1 == x;
with normalization rewrite;
next;
instantiate e\_\_8 == e\_\_2;
with enabled (applyOverride) prove;
use inCap[TASK][A := \dom  wait\_snd, B := \dom  wait\_rcv, x := topReady!];
prove;
next;
instantiate e\_\_9 == e\_\_3;
with enabled (applyOverride) prove;
next;
with normalization rewrite;
next;
instantiate x\_\_0 == x;
with normalization prove;
next;
with normalization rewrite;
next;
instantiate pt\_\_0 == pt;
with normalization rewrite;
next;
instantiate q\_\_0 == q;
prove;
next;
instantiate wrct == wr;
prove;
next;
with normalization rewrite;
next;
\end{zproof}

\begin{theorem}{QueueSendWS\_TQ\_vc\_ref}
\forall  QueueSendWS\_TQFSBSig | true @ \pre  QueueSendWS\_TQ
\end{theorem}

\begin{zproof}[QueueSendWS\_TQ\_vc\_ref]
with disabled (TaskQueue) prove by reduce;
instantiate running\_task' == topReady!;
prove;
use lQueueSendWS\_TQ\_Lemma;
prove;
instantiate wr\_\_0 == wrct;
prove;
with normalization rewrite;
\end{zproof}

\begin{zed}
QueueSend\_TQ \defs QueueSendN\_TQ \lor  QueueSendF\_TQ \lor  QueueSendW\_TQ \lor  QueueSendWS\_TQ
\end{zed}

\begin{schema}{QueueReceiveN\_TQ}
  \Delta TaskQueue\\
  que?: QUEUE\\
  topReady!: TASK
\where
  running\_task \notin  \dom  release\_snd\\
  running\_task \in  \dom  release\_rcv \implies  que? = release\_rcv(running\_task)\\
  que? \in  queue\\
  q\_size(que?) > 0\\
  que? \notin  \ran  wait\_snd\\
  \Xi Task\\
  queue' = queue\\
  q\_max' = q\_max\\
  q\_size' = q\_size \oplus  \{(que? \mapsto  q\_size(que?) - 1)\}\\
  \Xi WaitingData\\
  release\_snd' = release\_snd\\
  release\_rcv' = \{running\_task\} \ndres  release\_rcv\\
  topReady! = running\_task
\end{schema}

\begin{zproof}[QueueReceiveN\_TQ\$domainCheck]
prove by reduce;
\end{zproof}

\begin{schema}{QueueReceiveN\_TQFSBSig}
  TaskQueue\\
  que?: QUEUE
\where
  running\_task \notin  \dom  release\_snd\\
  running\_task \in  \dom  release\_rcv \implies  que? = release\_rcv(running\_task)\\
  que? \in  queue\\
  q\_size(que?) > 0\\
  que? \notin  \ran  wait\_snd
\end{schema}

\begin{zproof}[QueueReceiveN\_TQFSBSig\$domainCheck]
prove by reduce;
\end{zproof}

\begin{theorem}{QueueReceiveN\_TQ\_vc\_ref}
\forall  QueueReceiveN\_TQFSBSig | true @ \pre  QueueReceiveN\_TQ
\end{theorem}

\begin{zproof}[QueueReceiveN\_TQ\_vc\_ref]
prove by reduce;
use applyInRanPfun[QUEUE, \num ][A := QUEUE, B := \nat , f := q\_size, a := que?];
apply extensionality to predicate \dom  q\_max = \{que?\} \cup  \dom  q\_size;
apply extensionality to predicate \dom  release\_snd \cap  (\dom  release\_rcv \setminus  (state \inv  \limg  \{running\} \rimg )) = \{\};
apply extensionality to predicate \dom  release\_rcv \cap  \dom  release\_snd = \{\};
apply extensionality to predicate (\dom  release\_snd \cup  (\dom  release\_rcv \setminus  (state \inv  \limg  \{running\} \rimg ))) \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
apply extensionality to predicate (\dom  release\_rcv \cup  \dom  release\_snd) \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
with enabled (inPower) prove;
instantiate q\_\_0 == q;
instantiate x\_\_2 == x;
instantiate x\_\_3 == x\_\_0;
instantiate e\_\_3 == e;
split y = que?;
prove;
apply applyOverride;
with enabled (inRan) prove;
instantiate x\_\_6 == x\_\_2;
split x\_\_1 \in  \dom  release\_rcv \land  \lnot  state(x\_\_1) = running;
split q = que?;
prove;
\end{zproof}

\begin{schema}{QueueReceiveE\_TQ}
  \Delta TaskQueue\\
  que?: QUEUE\\
  topReady!: TASK
\where
  running\_task \notin  \dom  release\_snd\\
  running\_task \in  \dom  release\_rcv \implies  que? = release\_rcv(running\_task)\\
  que? \in  queue\\
  q\_size(que?) = 0\\
  running\_task \neq  idle\\
  state(topReady!) = ready\\
  \forall  t: state \inv  \limg  \{ready\} \rimg  @ priority(topReady!) \geq  priority(t)\\
  \exists  st?: STATE | st? = blocked @ Reschedule[topReady!/target?, tasks/tasks?, priority/pri?]\\
  \Xi QueueData\\
  wait\_snd' = wait\_snd\\
  wait\_rcv' = wait\_rcv \oplus  \{(running\_task \mapsto  que?)\}\\
  release\_snd' = release\_snd\\
  release\_rcv' = \{running\_task\} \ndres  release\_rcv
\end{schema}

\begin{zproof}[QueueReceiveE\_TQ\$domainCheck]
prove by reduce;
\end{zproof}

\begin{schema}{QueueReceiveE\_TQFSBSig}
  TaskQueue\\
  que?: QUEUE
\where
  running\_task \notin  \dom  release\_snd\\
  running\_task \in  \dom  release\_rcv \implies  que? = release\_rcv(running\_task)\\
  que? \in  queue\\
  q\_size(que?) = 0\\
  running\_task \neq  idle
\end{schema}

\begin{zproof}[QueueReceiveE\_TQFSBSig\$domainCheck]
prove by reduce;
\end{zproof}

\begin{theorem}{lQueueReceiveE\_TQ\_Lemma}
\forall  TaskQueue; que?: QUEUE; topReady!: TASK | running\_task \notin  \dom  release\_snd \land  (running\_task \in  \dom  release\_rcv \implies  que? = release\_rcv(running\_task)) \land  que? \in  queue \land  q\_size(que?) = 0 \land  running\_task \neq  idle \land  topReady! \in  state \inv  \limg  \{ready\} \rimg  \land  (\forall  rtsk: state \inv  \limg  \{ready\} \rimg  @ priority(topReady!) \geq  priority(rtsk)) @ \lnot  (TaskQueue[log\_context := log\_context \oplus  \{(running\_task, phys\_context)\}, phys\_context := log\_context(topReady!), release\_rcv := \{running\_task\} \ndres  release\_rcv, running\_task := topReady!, state := state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\}), wait\_rcv := wait\_rcv \oplus  \{(running\_task, que?)\}] \land  (st \in  TASK \land  \lnot  (state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) st = state(st) \implies  (state(st), (state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) st) \in  transition) \implies  t \in  TASK \land  state(t) = ready \land  \lnot  priority(topReady!) \geq  priority(t))
\end{theorem}

\begin{zproof}[lQueueReceiveE\_TQ\_Lemma]
prove by reduce;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
apply extensionality to predicate TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ) = TASK \setminus  ((state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{nonexistent\} \rimg );
apply extensionality to predicate (state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{running\} \rimg  = \{topReady!\};
prove;
apply applyOverride;
apply inPower;
prove;
cases;
apply extensionality to predicate \dom  wait\_snd \cap  ((state \inv  \limg  \{running\} \rimg ) \cup  \dom  wait\_rcv) = \{\};
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
prove;
instantiate e\_\_3 == x;
instantiate x\_\_1 == x;
prove;
next;
apply extensionality to predicate \dom  release\_snd \cap  (\dom  release\_rcv \setminus  (state \inv  \limg  \{running\} \rimg )) = \{\};
apply extensionality to predicate \dom  release\_rcv \cap  \dom  release\_snd = \{\};
prove;
instantiate x\_\_1 == x;
prove;
next;
apply extensionality to predicate (\dom  release\_snd \cup  (\dom  release\_rcv \setminus  (state \inv  \limg  \{running\} \rimg ))) \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
apply extensionality to predicate (\dom  release\_rcv \cup  \dom  release\_snd) \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
prove;
instantiate x\_\_1 == x;
with normalization rewrite;
next;
instantiate e\_\_4 == e;
apply oplusDef to expression wait\_rcv \oplus  \{(running\_task, que?)\};
with normalization prove;
with enabled (inRan) prove;
instantiate x\_\_1 == x;
prove;
next;
instantiate e\_\_6 == e\_\_0;
with enabled (inRan) prove;
instantiate x\_\_1 == x;
prove;
next;
with enabled (applyOverride) prove;
instantiate e\_\_4 == e\_\_1;
split e = running\_task;
prove;
next;
with enabled (applyOverride) prove;
instantiate e\_\_5 == e\_\_2;
split e = running\_task;
prove;
next;
with normalization rewrite;
next;
instantiate x == x\_\_0;
with normalization rewrite;
next;
prove;
next;
instantiate rtsk == pt;
split pt = running\_task;
prove;
next;
with normalization rewrite;
next;
instantiate rtsk == t;
prove;
next;
\end{zproof}

\begin{theorem}{QueueReceiveE\_TQ\_vc\_ref}
\forall  QueueReceiveE\_TQFSBSig | true @ \pre  QueueReceiveE\_TQ
\end{theorem}

\begin{zproof}[QueueReceiveE\_TQ\_vc\_ref]
use findDelegate[a := state \inv  \limg  \{ready\} \rimg, g := priority ];
with disabled (TaskQueue) prove by reduce;
instantiate running\_task' == f (state \inv  \limg  \{ready\} \rimg );
prove;
use lQueueReceiveE\_TQ\_Lemma[topReady! := f (state \inv  \limg  \{ready\} \rimg )];
prove;
instantiate t\_\_0 == rtsk;
prove;
with normalization rewrite;
\end{zproof}

\begin{schema}{QueueReceiveW\_TQ}
  \Delta TaskQueue\\
  que?: QUEUE\\
  topReady!: TASK
\where
  running\_task \notin  \dom  release\_snd\\
  running\_task \in  \dom  release\_rcv \implies  que? = release\_rcv(running\_task)\\
  que? \in  queue\\
  q\_size(que?) > 0\\
  topReady! \in  wait\_snd \inv  \limg  \{que?\} \rimg \\
  \forall  ws: wait\_snd \inv  \limg  \{que?\} \rimg  @ priority(topReady!) \geq  priority(ws)\\
  priority(topReady!) \leq  priority(running\_task)\\
  \Xi TaskData\\
  state' = state \oplus  \{(topReady! \mapsto  ready)\}\\
  \Xi ContextData\\
  \Xi PrioData\\
  queue' = queue\\
  q\_max' = q\_max\\
  q\_size' = q\_size \oplus  \{(que? \mapsto  q\_size(que?) - 1)\}\\
  wait\_snd' = \{topReady!\} \ndres  wait\_snd\\
  wait\_rcv' = wait\_rcv\\
  release\_snd' = release\_snd \oplus  \{(topReady! \mapsto  que?)\}\\
  release\_rcv' = \{running\_task\} \ndres  release\_rcv
\end{schema}

\begin{zproof}[QueueReceiveW\_TQ\$domainCheck]
prove by reduce;
\end{zproof}

\begin{schema}{QueueReceiveW\_TQFSBSig}
  TaskQueue\\
  que?: QUEUE
\where
  running\_task \notin  \dom  release\_snd\\
  running\_task \in  \dom  release\_rcv \implies  que? = release\_rcv(running\_task)\\
  que? \in  queue\\
  q\_size(que?) > 0\\
  \forall  ws: wait\_snd \inv  \limg  \{que?\} \rimg  @ priority(running\_task) \geq  priority(ws)
\end{schema}

\begin{zproof}[QueueReceiveW\_TQFSBSig\$domainCheck]
prove by reduce;
\end{zproof}

\begin{theorem}{lQueueReceiveW\_TQ\_Lemma}
\forall  TaskQueue; que?: QUEUE; topReady!: TASK | running\_task \notin  \dom  release\_snd \land  (running\_task \in  \dom  release\_rcv \implies  que? = release\_rcv(running\_task)) \land  que? \in  queue \land  q\_size(que?) > 0 \land  topReady! \in  wait\_snd \inv  \limg  \{que?\} \rimg  \land  (\forall  wsnt: wait\_snd \inv  \limg  \{que?\} \rimg  @ priority(topReady!) \geq  priority(wsnt)) \land  priority(running\_task) \geq  priority(topReady!) @ \lnot  (TaskQueue[q\_size := q\_size \oplus  \{(que?, (q\_size(que?) - 1))\}, release\_rcv := \{running\_task\} \ndres  release\_rcv, release\_snd := release\_snd \oplus  \{(topReady!, que?)\}, state := state \oplus  \{(topReady!, ready)\}, wait\_snd := \{topReady!\} \ndres  wait\_snd] \land  priority(topReady!) \leq  priority(running\_task) \land  (st \in  TASK \land  \lnot  (state \oplus  \{(topReady!, ready)\}) st = state(st) \implies  (state(st), (state \oplus  \{(topReady!, ready)\}) st) \in  transition) \implies  ws \in  \dom  wait\_snd \land  wait\_snd(ws) = que? \land  \lnot  priority(topReady!) \geq  priority(ws))
\end{theorem}

\begin{zproof}[lQueueReceiveW\_TQ\_Lemma]
prove by reduce;
apply extensionality to predicate TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ) = \{topReady!\} \cup  (TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ));
apply extensionality to predicate \dom  wait\_rcv \cap  (\dom  wait\_snd \setminus  \{topReady!\}) = \{\};
prove;
apply applyOverride;
apply inPower;
prove;
instantiate e\_\_8 == topReady!;
with enabled (runningUpdate) prove;
cases;
apply extensionality to predicate \dom  q\_max = \{wait\_snd(topReady!)\} \cup  \dom  q\_size;
with normalization prove;
next;
apply extensionality to predicate (\{topReady!\} \cup  \dom  release\_snd) \cap  (\dom  release\_rcv \setminus  (state \inv  \limg  \{running\} \rimg )) = \{\};
apply extensionality to predicate \dom  release\_rcv \cap  \dom  release\_snd = \{\};
apply extensionality to predicate (\dom  release\_rcv \cup  \dom  release\_snd) \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
prove;
instantiate x\_\_0 == x;
instantiate x\_\_1 == x;
prove;
next;
apply extensionality to predicate (\{topReady!\} \cup  (\dom  release\_snd \cup  (\dom  release\_rcv \setminus  (state \inv  \limg  \{running\} \rimg )))) \cap  (\dom  wait\_rcv \cup  (\dom  wait\_snd \setminus  \{topReady!\})) = \{\};
apply extensionality to predicate (\dom  release\_rcv \cup  \dom  release\_snd) \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
prove;
instantiate x\_\_0 == x;
instantiate x\_\_1 == x;
split x \in  \dom  wait\_rcv;
prove;
next;
instantiate e\_\_4 == e;
with enabled (inRan) prove;
instantiate x\_\_0 == x;
prove;
next;
instantiate e\_\_6 == e\_\_0;
apply oplusDef to expression release\_snd \oplus  \{(topReady!, wait\_snd(topReady!))\};
with enabled (inRan) prove;
instantiate x\_\_0 == x;
with normalization rewrite;
next;
instantiate e\_\_7 == e\_\_1;
with enabled (inRan) prove;
instantiate x\_\_0 == x;
prove;
next;
instantiate e\_\_8 == e\_\_2;
prove;
next;
instantiate e\_\_9 == e\_\_3;
with enabled (applyOverride) prove;
use inCap[TASK][A := \dom  wait\_snd, B := \dom  wait\_rcv, x := topReady!];
prove;
next;
with normalization rewrite;
next;
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
instantiate x\_\_0 == x;
prove;
next;
instantiate pt\_\_0 == pt;
with normalization rewrite;
next;
instantiate q\_\_0 == q;
prove;
next;
invoke transition;
prove;
next;
instantiate wsnt == ws;
prove;
next;
\end{zproof}

\begin{theorem}{QueueReceiveW\_TQ\_vc\_ref}
\forall  QueueReceiveW\_TQFSBSig | true @ \pre  QueueReceiveW\_TQ
\end{theorem}

\begin{zproof}[QueueReceiveW\_TQ\_vc\_ref]
use findDelegate[a := wait\_snd \inv  \limg  \{que?\} \rimg, g := priority ];
with disabled (TaskQueue) prove by reduce;
instantiate topReady! == f (wait\_snd \inv  \limg  \{que?\} \rimg );
prove;
use lQueueReceiveW\_TQ\_Lemma[topReady! := f (wait\_snd \inv  \limg  \{que?\} \rimg )];
prove;
instantiate ws\_\_0 == f (wait\_snd \inv  \limg  \{que?\} \rimg );
instantiate t == wsnt;
with normalization rewrite;
\end{zproof}

\begin{schema}{QueueReceiveWS\_TQ}
  \Delta TaskQueue\\
  que?: QUEUE\\
  topReady!: TASK
\where
  running\_task \notin  \dom  release\_snd\\
  running\_task \in  \dom  release\_rcv \implies  que? = release\_rcv(running\_task)\\
  que? \in  queue\\
  q\_size(que?) > 0\\
  topReady! \in  wait\_snd \inv  \limg  \{que?\} \rimg \\
  \forall  ws: wait\_snd \inv  \limg  \{que?\} \rimg  @ priority(topReady!) \geq  priority(ws)\\
  priority(topReady!) > priority(running\_task)\\
  \exists  st?: STATE | st? = ready @ Reschedule[topReady!/target?, tasks/tasks?, priority/pri?]\\
  queue' = queue\\
  q\_max' = q\_max\\
  q\_size' = q\_size \oplus  \{(que? \mapsto  q\_size(que?) - 1)\}\\
  wait\_snd' = \{topReady!\} \ndres  wait\_snd\\
  wait\_rcv' = wait\_rcv\\
  release\_snd' = release\_snd \oplus  \{(topReady! \mapsto  que?)\}\\
  release\_rcv' = \{running\_task\} \ndres  release\_rcv
\end{schema}

\begin{zproof}[QueueReceiveWS\_TQ\$domainCheck]
prove by reduce;
\end{zproof}

\begin{schema}{QueueReceiveWS\_TQFSBSig}
  TaskQueue\\
  que?: QUEUE
\where
  running\_task \notin  \dom  release\_snd\\
  running\_task \in  \dom  release\_rcv \implies  que? = release\_rcv(running\_task)\\
  que? \in  queue\\
  q\_size(que?) > 0\\
  \exists  topReady!: wait\_snd \inv  \limg  \{que?\} \rimg  | \forall  ws: wait\_snd \inv  \limg  \{que?\} \rimg  @ priority(topReady!) \geq  priority(ws) @ priority(topReady!) > priority(running\_task)
\end{schema}

\begin{zproof}[QueueReceiveWS\_TQFSBSig\$domainCheck]
prove by reduce;
\end{zproof}

\begin{theorem}{lQueueReceiveWS\_TQ\_Lemma}
\forall  TaskQueue; que?: QUEUE; topReady!: TASK | running\_task \notin  \dom  release\_snd \land  (running\_task \in  \dom  release\_rcv \implies  que? = release\_rcv(running\_task)) \land  que? \in  queue \land  q\_size(que?) > 0 \land  topReady! \in  wait\_snd \inv  \limg  \{que?\} \rimg  \land  (\forall  wsnt: wait\_snd \inv  \limg  \{que?\} \rimg  @ priority(topReady!) \geq  priority(wsnt)) \land  priority(topReady!) > priority(running\_task) @ \lnot  (TaskQueue[log\_context := log\_context \oplus  \{(running\_task, phys\_context)\}, phys\_context := log\_context(topReady!), q\_size := q\_size \oplus  \{(wait\_snd(topReady!), (q\_size (wait\_snd(topReady!)) - 1))\}, release\_rcv := \{running\_task\} \ndres  release\_rcv, release\_snd := release\_snd \oplus  \{(topReady!, wait\_snd(topReady!))\}, running\_task := topReady!, state := state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\}), wait\_snd := \{topReady!\} \ndres  wait\_snd] \land  (st \in  TASK \land  \lnot  (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) st = state(st) \implies  (state(st), (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) st) \in  transition) \implies  ws \in  \dom  wait\_snd \land  wait\_snd(ws) = wait\_snd(topReady!) \land  \lnot  priority(topReady!) \geq  priority(ws))
\end{theorem}

\begin{zproof}[lQueueReceiveWS\_TQ\_Lemma]
prove by reduce;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
apply extensionality to predicate TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ) = \{topReady!\} \cup  (TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ) \cup  (state \inv  \limg  \{running\} \rimg ));
apply extensionality to predicate (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{running\} \rimg  = \{topReady!\};
prove;
apply applyOverride;
apply inPower;
instantiate e\_\_3 == topReady!;
prove;
cases;
apply extensionality to predicate \dom  q\_max = \{wait\_snd(topReady!)\} \cup  \dom  q\_size;
with normalization prove;
next;
apply extensionality to predicate \dom  wait\_rcv \cap  (\dom  wait\_snd \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{running\} \rimg )) = \{\};
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
with enabled (applyOverride) prove;
instantiate x\_\_1 == x;
prove;
next;
apply extensionality to predicate (((state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{running\} \rimg ) \cup  \dom  release\_snd) \cap  (\dom  release\_rcv \setminus  (state \inv  \limg  \{running\} \rimg )) = \{\};
apply extensionality to predicate \dom  release\_rcv \cap  \dom  release\_snd = \{\};
apply extensionality to predicate (\dom  release\_rcv \cup  \dom  release\_snd) \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
with enabled (applyOverride) prove;
instantiate x\_\_1 == x;
instantiate x\_\_2 == x;
prove;
next;
apply extensionality to predicate (((state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{running\} \rimg ) \cup  (\dom  release\_snd \cup  (\dom  release\_rcv \setminus  (state \inv  \limg  \{running\} \rimg )))) \cap  (\dom  wait\_rcv \cup  (\dom  wait\_snd \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{running\} \rimg ))) = \{\};
apply extensionality to predicate (\dom  release\_rcv \cup  \dom  release\_snd) \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
prove;
apply applyOverride;
instantiate x\_\_0 == x;
instantiate x\_\_1 == x;
instantiate x\_\_2 == x;
with normalization rewrite;
next;
instantiate e\_\_4 == e;
with enabled (inRan) prove;
instantiate x\_\_1 == x;
prove;
next;
instantiate e\_\_6 == e\_\_0;
apply oplusDef to expression release\_snd \oplus  \{(topReady!, wait\_snd(topReady!))\};
with enabled (inRan) prove;
instantiate x\_\_1 == x;
with normalization rewrite;
next;
instantiate e\_\_7 == e\_\_1;
with enabled (inRan) prove;
instantiate x\_\_1 == x;
prove;
next;
instantiate e\_\_8 == e\_\_2;
with enabled (applyOverride) prove;
next;
instantiate e\_\_9 == e\_\_3;
with enabled (applyOverride) prove;
use inCap[TASK][A := \dom  wait\_snd, B := \dom  wait\_rcv, x := topReady!];
prove;
next;
with normalization rewrite;
next;
instantiate x\_\_0 == x;
with normalization prove;
next;
with normalization rewrite;
next;
instantiate pt\_\_0 == pt;
with normalization rewrite;
next;
instantiate q\_\_0 == q;
prove;
next;
with normalization rewrite;
next;
instantiate wsnt == ws;
prove;
next;
\end{zproof}

\begin{theorem}{QueueReceiveWS\_TQ\_vc\_ref}
\forall  QueueReceiveWS\_TQFSBSig | true @ \pre  QueueReceiveWS\_TQ
\end{theorem}

\begin{zproof}[QueueReceiveWS\_TQ\_vc\_ref]
with disabled (TaskQueue) prove by reduce;
instantiate running\_task' == topReady!;
prove;
use lQueueReceiveWS\_TQ\_Lemma;
prove;
instantiate ws\_\_0 == wsnt;
prove;
with normalization rewrite;
\end{zproof}

\begin{zed}
QueueReceive\_TQ \defs QueueReceiveN\_TQ \lor  QueueReceiveE\_TQ \lor  QueueReceiveW\_TQ \lor  QueueReceiveWS\_TQ
\end{zed}

\begin{axdef}
  slice\_delay: \nat 
\where
  \Label{disabled slice_delay_def}  slice\_delay = 1
\end{axdef}

\begin{schema}{Time}
  clock: \nat \\
  delayed\_task: \power  TASK\\
  time: TASK \pfun  \nat \\
  time\_slice: \nat 
\where
  \forall  t: \dom  time @ time(t) \geq  clock
\end{schema}

\begin{zproof}[Time\$domainCheck]
 prove;
\end{zproof}

\begin{schema}{Init\_Time}
  Time~'
\where
  clock' = 0\\
  delayed\_task' = \emptyset\\
  time' = \emptyset\\
  time\_slice' = slice\_delay
\end{schema}

\begin{theorem}{TimeInit}
\exists  Time~' @ Init\_Time
\end{theorem}

\begin{zproof}[TimeInit]
 prove by reduce;
\end{zproof}

\begin{schema}{TaskQueueTime}
  TaskQueue\\
  Time
\where
  \langle delayed\_task, \dom  wait\_snd, \dom  wait\_rcv\rangle  \partition  \dom  time\\
  delayed\_task \subseteq  state \inv  \limg  \{blocked\} \rimg 
\end{schema}

\begin{theorem}{rule domTime}
\forall  TaskQueueTime; t: TASK | t \in  \dom  time @ t \in  state \inv  \limg  \{blocked\} \rimg 
\end{theorem}

\begin{zproof}[domTime]
invoke TaskQueueTime;
invoke TaskQueue;
prove;
apply extensionality to predicate delayed\_task \cup  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \dom  time;
instantiate y == t;
with enabled (inPower) prove;
instantiate e == t;
instantiate e\_\_0 == t;
instantiate e\_\_1 == t;
with normalization rewrite;
\end{zproof}

\begin{schema}{Init\_TaskQueueTime}
  TaskQueueTime~'
\where
  Init\_TaskQueue\\
  Init\_Time
\end{schema}

\begin{theorem}{TaskQueueTimeInit}
\exists  TaskQueueTime~' @ Init\_TaskQueueTime
\end{theorem}

\begin{zproof}[TaskQueueTimeInit]
 use TaskQueueInit;
with enabled (disjointCat) prove by reduce;
\end{zproof}

\begin{zed}
\Delta TaskQueueTime \defs TaskQueueTime \land  TaskQueueTime~' \land  \Delta Task
\end{zed}

\begin{schema}{ExtendTaskQueueXi}
  \Delta TaskQueueTime
\where
  \Xi Time
\end{schema}

\begin{zed}
CreateTaskN\_TQT \defs ExtendTaskQueueXi \land  CreateTaskN\_TQ
\end{zed}

\begin{zed}
CreateTaskN\_TQTFSBSig \defs TaskQueueTime \land  CreateTaskN\_TQFSBSig
\end{zed}

\begin{theorem}{CreateTaskN\_TQT\_vc\_ref}
\forall  CreateTaskN\_TQTFSBSig | true @ \pre  CreateTaskN\_TQT
\end{theorem}

\begin{zproof}[CreateTaskN\_TQT\_vc\_ref]
use CreateTaskN\_TQ\_vc\_ref;
with disabled (TaskQueue) prove by reduce;
apply inPower to predicate delayed\_task \in  \power  ((state \oplus  \{(target?, ready)\}) \inv  \limg  \{blocked\} \rimg );
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
prove;
instantiate e\_\_0 == e;
with enabled (applyOverride) prove;
\end{zproof}

\begin{zed}
CreateTaskS\_TQT \defs ExtendTaskQueueXi \land  CreateTaskS\_TQ
\end{zed}

\begin{zed}
CreateTaskS\_TQTFSBSig \defs TaskQueueTime \land  CreateTaskS\_TQFSBSig
\end{zed}

\begin{theorem}{CreateTaskS\_TQT\_vc\_ref}
\forall  CreateTaskS\_TQTFSBSig | true @ \pre  CreateTaskS\_TQT
\end{theorem}

\begin{zproof}[CreateTaskS\_TQT\_vc\_ref]
use CreateTaskS\_TQ\_vc\_ref;
with disabled (TaskQueue) prove by reduce;
instantiate st\_\_0 == st;
with disabled (Queue, TaskData, PrioData, ContextData) prove by reduce;
apply inPower to predicate delayed\_task \in  \power  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(target?, running)\})) \inv  \limg  \{blocked\} \rimg );
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
prove;
instantiate e\_\_0 == e;
prove;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
prove;
\end{zproof}

\begin{zed}
CreateTask\_TQT \defs CreateTaskN\_TQT \lor  CreateTaskS\_TQT
\end{zed}

\begin{schema}{DeleteTaskN\_TQT}
  DeleteTaskN\_TQ\\
  \Delta TaskQueueTime
\where
  clock' = clock\\
  delayed\_task' = delayed\_task \setminus  \{target?\}\\
  time' = \{target?\} \ndres  time\\
  time\_slice' = time\_slice
\end{schema}

\begin{zed}
DeleteTaskN\_TQTFSBSig \defs TaskQueueTime \land  DeleteTaskN\_TQFSBSig
\end{zed}

\begin{theorem}{DeleteTaskN\_TQT\_vc\_ref}
\forall  DeleteTaskN\_TQTFSBSig | true @ \pre  DeleteTaskN\_TQT
\end{theorem}

\begin{zproof}[DeleteTaskN\_TQT\_vc\_ref]
use DeleteTaskN\_TQ\_vc\_ref;
with disabled (TaskQueue, partitionDef) prove by reduce;
cases;
with enabled (disjointCat) prove;
apply extensionality to predicate (\dom  wait\_rcv \setminus  \{target?\}) \cap  (\dom  wait\_snd \setminus  \{target?\}) = \{\};
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
apply extensionality to predicate (delayed\_task \setminus  \{target?\}) \cap  (\dom  wait\_rcv \setminus  \{target?\} \cup  (\dom  wait\_snd \setminus  \{target?\})) = \{\};
apply extensionality to predicate delayed\_task \setminus  \{target?\} \cup  (\dom  wait\_rcv \setminus  \{target?\} \cup  (\dom  wait\_snd \setminus  \{target?\})) = delayed\_task \cup  (\dom  wait\_rcv \cup  \dom  wait\_snd) \setminus  \{target?\};
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
prove;
instantiate x\_\_1 == x;
instantiate x\_\_2 == x\_\_0;
prove;
next;
apply inPower to predicate delayed\_task \setminus  \{target?\} \in  \power  ((state \oplus  \{(target?, nonexistent)\}) \inv  \limg  \{blocked\} \rimg );
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
prove;
instantiate e\_\_0 == e;
prove;
next;
instantiate pt\_\_0 == pt;
apply applyOverride to expression (state \oplus  \{(target?, nonexistent)\}) pt;
prove;
next;
with enabled (applyOverride) prove;
next;
instantiate t\_\_0 == t;
prove;
next;
\end{zproof}

\begin{zed}
DeleteTaskS\_TQT \defs ExtendTaskQueueXi \land  DeleteTaskS\_TQ
\end{zed}

\begin{zed}
DeleteTaskS\_TQTFSBSig \defs TaskQueueTime \land  DeleteTaskS\_TQFSBSig
\end{zed}

\begin{theorem}{lDeleteTaskS\_TQT\_Lemma}
\forall  TaskQueueTime; topReady!, target?: TASK | running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv \land  target? \in  tasks \setminus  \{idle\} \land  state(target?) \in  \{running\} \land  state(topReady!) = ready \land  (\forall  rtsk: state \inv  \limg  \{ready\} \rimg  @ priority(topReady!) \geq  priority(rtsk)) @ \lnot  (TaskQueueTime[log\_context := log\_context \oplus  \{(target?, bare\_context)\}, phys\_context := log\_context(topReady!), running\_task := topReady!, state := state \oplus  (\{(target?, nonexistent)\} \cup  \{(topReady!, running)\}), tasks := tasks \setminus  \{target?\}] \land  (st \in  TASK \land  \lnot  (state \oplus  (\{(target?, nonexistent)\} \cup  \{(topReady!, running)\})) st = state(st) \implies  (state(st), (state \oplus  (\{(target?, nonexistent)\} \cup  \{(topReady!, running)\})) st) \in  transition) \implies  t \in  TASK \land  state(t) = ready \land  \lnot  priority(topReady!) \geq  priority(t))
\end{theorem}

\begin{zproof}[lDeleteTaskS\_TQT\_Lemma]
with disabled (TaskQueue) prove by reduce;
use lDeleteTaskS\_TQ\_Lemma;
prove;
instantiate rtsk\_\_0 == rtsk;
prove;
with disabled (Queue, TaskData, PrioData, ContextData) prove by reduce;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
apply inPower to predicate delayed\_task \in  \power  ((state \oplus  (\{(target?, nonexistent)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{blocked\} \rimg );
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
prove;
instantiate e\_\_0 == e;
instantiate rtsk\_\_0 == t;
with enabled (applyOverride) prove;
\end{zproof}

\begin{theorem}{DeleteTaskS\_TQT\_vc\_ref}
\forall  DeleteTaskS\_TQTFSBSig | true @ \pre  DeleteTaskS\_TQT
\end{theorem}

\begin{zproof}[DeleteTaskS\_TQT\_vc\_ref]
use findDelegate[a := state \inv  \limg  \{ready\} \rimg , g := priority];
with disabled (TaskQueueTime) prove by reduce;
instantiate running\_task' == f (state \inv  \limg  \{ready\} \rimg );
prove;
use lDeleteTaskS\_TQT\_Lemma[topReady! := f (state \inv  \limg  \{ready\} \rimg )];
prove;
instantiate t\_\_0 == rtsk;
prove;
\end{zproof}

\begin{zed}
DeleteTask\_TQT \defs DeleteTaskN\_TQT \lor  DeleteTaskS\_TQT
\end{zed}

\begin{zed}
ExecuteRunningTask\_TQT \defs ExtendTaskQueueXi \land  ExecuteRunningTask\_TQ
\end{zed}

\begin{zed}
ExecuteRunningTask\_TQTFSBSig \defs TaskQueueTime \land  ExecuteRunningTask\_TQFSBSig
\end{zed}

\begin{theorem}{ExecuteRunningTask\_TQT\_vc\_ref}
\forall  ExecuteRunningTask\_TQTFSBSig | true @ \pre  ExecuteRunningTask\_TQT
\end{theorem}

\begin{zproof}[ExecuteRunningTask\_TQT\_vc\_ref]
 with disabled (TaskData, StateData, PrioData, Queue, Time) reduce;
\end{zproof}

\begin{schema}{SuspendTaskN\_TQT}
  SuspendTaskN\_TQ\\
  \Delta TaskQueueTime
\where
  clock' = clock\\
  delayed\_task' = delayed\_task \setminus  \{target?\}\\
  time' = \{target?\} \ndres  time\\
  time\_slice' = time\_slice
\end{schema}

\begin{zed}
SuspendTaskN\_TQTFSBSig \defs TaskQueueTime \land  SuspendTaskN\_TQFSBSig
\end{zed}

\begin{theorem}{SuspendTaskN\_TQT\_vc\_ref}
\forall  SuspendTaskN\_TQTFSBSig | true @ \pre  SuspendTaskN\_TQT
\end{theorem}

\begin{zproof}[SuspendTaskN\_TQT\_vc\_ref]
use SuspendTaskN\_TQ\_vc\_ref;
with disabled (TaskQueue, partitionDef) prove by reduce;
cases;
with disabled (Queue, PrioData, StateData, ContextData) prove by reduce;
next;
with enabled (disjointCat) prove;
apply extensionality to predicate (\dom  wait\_rcv \setminus  \{target?\}) \cap  (\dom  wait\_snd \setminus  \{target?\}) = \{\};
apply extensionality to predicate (delayed\_task \setminus  \{target?\}) \cap  (\dom  wait\_rcv \setminus  \{target?\} \cup  (\dom  wait\_snd \setminus  \{target?\})) = \{\};
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
apply extensionality to predicate delayed\_task \setminus  \{target?\} \cup  (\dom  wait\_rcv \setminus  \{target?\} \cup  (\dom  wait\_snd \setminus  \{target?\})) = delayed\_task \cup  (\dom  wait\_rcv \cup  \dom  wait\_snd) \setminus  \{target?\};
prove;
instantiate x\_\_1 == x;
instantiate x\_\_2 == x\_\_0;
prove;
next;
apply inPower to predicate delayed\_task \setminus  \{target?\} \in  \power  ((state \oplus  \{(target?, suspended)\}) \inv  \limg  \{blocked\} \rimg );
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
prove;
instantiate e\_\_0 == e;
prove;
next;
instantiate pt\_\_0 == pt;
with enabled (applyOverride) prove;
next;
instantiate st\_\_0 == st;
prove;
next;
instantiate t\_\_0 == t;
prove;
next;
\end{zproof}

\begin{zed}
SuspendTaskS\_TQT \defs ExtendTaskQueueXi \land  SuspendTaskS\_TQ
\end{zed}

\begin{zed}
SuspendTaskS\_TQTFSBSig \defs TaskQueueTime \land  SuspendTaskS\_TQFSBSig
\end{zed}

\begin{theorem}{lSuspendTaskS\_TQT\_Lemma}
\forall  TaskQueueTime; target?, topReady!: TASK | running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv \land  target? \in  tasks \setminus  \{idle\} \land  state(target?) \in  \{running\} \land  state(topReady!) = ready \land  (\forall  rtsk: state \inv  \limg  \{ready\} \rimg  @ priority(topReady!) \geq  priority(rtsk)) @ \lnot  (TaskQueueTime[log\_context := log\_context \oplus  \{(running\_task, phys\_context)\}, phys\_context := log\_context(topReady!), running\_task := topReady!, state := state \oplus  (\{(running\_task, suspended)\} \cup  \{(topReady!, running)\})] \land  (st \in  TASK \land  \lnot  (state \oplus  (\{(running\_task, suspended)\} \cup  \{(topReady!, running)\})) st = state(st) \implies  (state(st), (state \oplus  (\{(running\_task, suspended)\} \cup  \{(topReady!, running)\})) st) \in  transition) \implies  t \in  TASK \land  state(t) = ready \land  \lnot  priority(topReady!) \geq  priority(t))
\end{theorem}

\begin{zproof}[lSuspendTaskS\_TQT\_Lemma]
use lSuspendTaskS\_TQ\_Lemma;
with disabled (TaskQueue) prove by reduce;
instantiate rtsk\_\_0 == rtsk;
prove;
with disabled (TaskData, PrioData, ContextData, Queue) reduce;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
apply inPower to predicate delayed\_task \in  \power  ((state \oplus  (\{(running\_task, suspended)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{blocked\} \rimg );
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
prove;
instantiate e\_\_0 == e;
instantiate rtsk\_\_0 == t;
with enabled (applyOverride) prove;
\end{zproof}

\begin{theorem}{SuspendTaskS\_TQT\_vc\_ref}
\forall  SuspendTaskS\_TQTFSBSig | true @ \pre  SuspendTaskS\_TQT
\end{theorem}

\begin{zproof}[SuspendTaskS\_TQT\_vc\_ref]
use findDelegate[a := state \inv  \limg  \{ready\} \rimg , g := priority];
with disabled (TaskQueueTime) prove by reduce;
instantiate running\_task' == f (state \inv  \limg  \{ready\} \rimg );
prove;
use lSuspendTaskS\_TQT\_Lemma[topReady! := f (state \inv  \limg  \{ready\} \rimg )];
prove;
instantiate t\_\_0 == rtsk;
prove;
\end{zproof}

\begin{zed}
SuspendTaskO\_TQT \defs ExtendTaskQueueXi \land  SuspendTaskO\_TQ
\end{zed}

\begin{zed}
SuspendTaskO\_TQTFSBSig \defs TaskQueueTime \land  SuspendTaskO\_TQFSBSig
\end{zed}

\begin{theorem}{SuspendTaskO\_TQT\_vc\_ref}
\forall  SuspendTaskO\_TQTFSBSig | true @ \pre  SuspendTaskO\_TQT
\end{theorem}

\begin{zproof}[SuspendTaskO\_TQT\_vc\_ref]
with disabled (TaskQueueTime) prove by reduce;
\end{zproof}

\begin{zed}
SuspendTask\_TQT \defs SuspendTaskN\_TQT \lor  SuspendTaskS\_TQT \lor  SuspendTaskO\_TQT
\end{zed}

\begin{zed}
ResumeTaskN\_TQT \defs ExtendTaskQueueXi \land  ResumeTaskN\_TQ
\end{zed}

\begin{zed}
ResumeTaskN\_TQTFSBSig \defs TaskQueueTime \land  ResumeTaskN\_TQFSBSig
\end{zed}

\begin{theorem}{ResumeTaskN\_TQT\_vc\_ref}
\forall  ResumeTaskN\_TQTFSBSig | true @ \pre  ResumeTaskN\_TQT
\end{theorem}

\begin{zproof}[ResumeTaskN\_TQT\_vc\_ref]
use ResumeTaskN\_TQ\_vc\_ref;
with disabled (TaskQueue) prove by reduce;
instantiate st\_\_0 == st;
apply inPower to predicate delayed\_task \in  \power  ((state \oplus  \{(target?, ready)\}) \inv  \limg  \{blocked\} \rimg );
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
with disabled (Queue, TaskData, PrioData, ContextData) prove by reduce;
instantiate e\_\_0 == e;
with enabled (applyOverride) prove;
\end{zproof}

\begin{zed}
ResumeTaskS\_TQT \defs ExtendTaskQueueXi \land  ResumeTaskS\_TQ
\end{zed}

\begin{zed}
ResumeTaskS\_TQTFSBSig \defs TaskQueueTime \land  ResumeTaskS\_TQFSBSig
\end{zed}

\begin{theorem}{ResumeTaskS\_TQT\_vc\_ref}
\forall  ResumeTaskS\_TQTFSBSig | true @ \pre  ResumeTaskS\_TQT
\end{theorem}

\begin{zproof}[ResumeTaskS\_TQT\_vc\_ref]
use ResumeTaskS\_TQ\_vc\_ref;
with disabled (TaskQueue) prove by reduce;
instantiate st\_\_0 == st;
apply inPower to predicate delayed\_task \in  \power  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(target?, running)\})) \inv  \limg  \{blocked\} \rimg );
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
with disabled (TaskData, PrioData, ContextData, Queue) prove by reduce;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
instantiate e\_\_0 == e;
prove;
\end{zproof}

\begin{zed}
ResumeTask\_TQT \defs ResumeTaskN\_TQT \lor  ResumeTaskS\_TQT
\end{zed}

\begin{zed}
ChangeTaskPriorityN\_TQT \defs ExtendTaskQueueXi \land  ChangeTaskPriorityN\_TQ
\end{zed}

\begin{zed}
ChangeTaskPriorityN\_TQTFSBSig \defs TaskQueueTime \land  ChangeTaskPriorityN\_TQFSBSig
\end{zed}

\begin{theorem}{ChangeTaskPriorityN\_TQT\_vc\_ref}
\forall  ChangeTaskPriorityN\_TQTFSBSig | true @ \pre  ChangeTaskPriorityN\_TQT
\end{theorem}

\begin{zproof}[ChangeTaskPriorityN\_TQT\_vc\_ref]
with enabled (applyOverride) prove by reduce;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
instantiate t\_\_0 == pt;
with normalization rewrite;
\end{zproof}

\begin{zed}
ChangeTaskPriorityS\_TQT \defs ExtendTaskQueueXi \land  ChangeTaskPriorityS\_TQ
\end{zed}

\begin{zed}
ChangeTaskPriorityS\_TQTFSBSig \defs TaskQueueTime \land  ChangeTaskPriorityS\_TQFSBSig
\end{zed}

\begin{theorem}{ChangeTaskPriorityS\_TQT\_vc\_ref}
\forall  ChangeTaskPriorityS\_TQTFSBSig | true @ \pre  ChangeTaskPriorityS\_TQT
\end{theorem}

\begin{zproof}[ChangeTaskPriorityS\_TQT\_vc\_ref]
use ChangeTaskPriorityS\_TQ\_vc\_ref;
with disabled (TaskQueue) prove by reduce;
instantiate st\_\_0 == st;
apply inPower to predicate delayed\_task \in  \power  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(target?, running)\})) \inv  \limg  \{blocked\} \rimg );
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
with disabled (TaskData, PrioData, ContextData, Queue) prove by reduce;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
instantiate e\_\_0 == e;
prove;
\end{zproof}

\begin{zed}
ChangeTaskPriorityD\_TQT \defs ExtendTaskQueueXi \land  ChangeTaskPriorityD\_TQ
\end{zed}

\begin{zed}
ChangeTaskPriorityD\_TQTFSBSig \defs TaskQueueTime \land  ChangeTaskPriorityD\_TQFSBSig
\end{zed}

\begin{theorem}{lChangeTaskPriorityD\_TQT\_Lemma}
\forall  TaskQueueTime; target?, topReady!: TASK; newpri?: \nat  | state(target?) = running \land  (target? = idle \implies  newpri? = 0) \land  state(topReady!) = ready \land  (\forall  rtsk: state \inv  \limg  \{ready\} \rimg  @ priority(topReady!) \geq  priority(rtsk)) \land  newpri? < priority(topReady!) @ \lnot  (TaskQueueTime[log\_context := log\_context \oplus  \{(running\_task, phys\_context)\}, phys\_context := log\_context(topReady!), priority := priority \oplus  \{(target?, newpri?)\}, running\_task := topReady!, state := state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})] \land  newpri? < priority(topReady!) \land  (st \in  TASK \land  \lnot  (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) st = state(st) \implies  (state(st), (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) st) \in  transition) \implies  t \in  TASK \land  state(t) = ready \land  \lnot  priority(topReady!) \geq  priority(t))
\end{theorem}

\begin{zproof}[lChangeTaskPriorityD\_TQT\_Lemma]
use lChangeTaskPriorityD\_TQ\_Lemma;
with disabled (TaskQueue) prove by reduce;
instantiate rtsk\_\_0 == rtsk;
prove;
with disabled (TaskData, PrioData, ContextData, Queue) reduce;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
apply inPower to predicate delayed\_task \in  \power  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{blocked\} \rimg );
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
prove;
instantiate e\_\_0 == e;
instantiate rtsk\_\_0 == t;
with enabled (applyOverride) prove;
\end{zproof}

\begin{theorem}{ChangeTaskPriorityD\_TQT\_vc\_ref}
\forall  ChangeTaskPriorityD\_TQTFSBSig | true @ \pre  ChangeTaskPriorityD\_TQT
\end{theorem}

\begin{zproof}[ChangeTaskPriorityD\_TQT\_vc\_ref]
use findDelegate[a := state \inv  \limg  \{ready\} \rimg , g := priority];
with disabled (TaskQueueTime) prove by reduce;
instantiate running\_task' == f (state \inv  \limg  \{ready\} \rimg );
prove;
use lChangeTaskPriorityD\_TQT\_Lemma[topReady! := f (state \inv  \limg  \{ready\} \rimg )];
prove;
instantiate t\_\_0 == readyTask;
instantiate t\_\_0 == rtsk;
instantiate t\_\_0 == t;
prove;
\end{zproof}

\begin{zed}
CreateQueue\_TQT \defs ExtendTaskQueueXi \land  CreateQueue\_TQ
\end{zed}

\begin{zed}
CreateQueue\_TQTFSBSig \defs TaskQueueTime \land  CreateQueue\_TQFSBSig
\end{zed}

\begin{theorem}{CreateQueue\_TQT\_vc\_ref}
\forall  CreateQueue\_TQTFSBSig | true @ \pre  CreateQueue\_TQT
\end{theorem}

\begin{zproof}[CreateQueue\_TQT\_vc\_ref]
 use CreateQueue\_TQ\_vc\_ref;
with disabled (TaskQueue) prove by reduce;
\end{zproof}

\begin{zed}
DeleteQueue\_TQT \defs ExtendTaskQueueXi \land  DeleteQueue\_TQ
\end{zed}

\begin{zed}
DeleteQueue\_TQTFSBSig \defs TaskQueueTime \land  DeleteQueue\_TQFSBSig
\end{zed}

\begin{theorem}{DeleteQueue\_TQT\_vc\_ref}
\forall  DeleteQueue\_TQTFSBSig | true @ \pre  DeleteQueue\_TQT
\end{theorem}

\begin{zproof}[DeleteQueue\_TQT\_vc\_ref]
 use DeleteQueue\_TQ\_vc\_ref;
with disabled (TaskQueue) prove by reduce;
\end{zproof}

\begin{zed}
QueueSendN\_TQT \defs ExtendTaskQueueXi \land  QueueSendN\_TQ
\end{zed}

\begin{zed}
QueueSendN\_TQTFSBSig \defs TaskQueueTime \land  QueueSendN\_TQFSBSig
\end{zed}

\begin{theorem}{QueueSendN\_TQT\_vc\_ref}
\forall  QueueSendN\_TQTFSBSig | true @ \pre  QueueSendN\_TQT
\end{theorem}

\begin{zproof}[QueueSendN\_TQT\_vc\_ref]
use QueueSendN\_TQ\_vc\_ref;
with disabled (TaskQueue) prove by reduce;
\end{zproof}

\begin{schema}{QueueSendF\_TQT}
  \Delta TaskQueueTime\\
  QueueSendF\_TQ\\
  n?: \nat 
\where
  n? > clock\\
  clock' = clock\\
  delayed\_task' = delayed\_task\\
  time' = time \oplus  \{(running\_task \mapsto  n?)\}\\
  time\_slice' = time\_slice
\end{schema}

\begin{schema}{QueueSendF\_TQTFSBSig}
  TaskQueueTime\\
  QueueSendF\_TQFSBSig\\
  n?: \nat 
\where
  n? > clock
\end{schema}

\begin{theorem}{lQueueSendF\_TQT\_Lemma}
\forall  TaskQueueTime; topReady!: TASK; que?: QUEUE; n?: \nat  | running\_task \notin  \dom  release\_rcv \land  (running\_task \in  \dom  release\_snd \implies  que? = release\_snd(running\_task)) \land  que? \in  queue \land  q\_size(que?) = q\_max(que?) \land  running\_task \neq  idle \land  state(topReady!) = ready \land  (\forall  rtsk: state \inv  \limg  \{ready\} \rimg  @ priority(topReady!) \geq  priority(rtsk)) \land  n? > clock @ \lnot  (TaskQueueTime[log\_context := log\_context \oplus  \{(running\_task, phys\_context)\}, phys\_context := log\_context(topReady!), release\_snd := \{running\_task\} \ndres  release\_snd, running\_task := topReady!, state := state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\}), time := time \oplus  \{(running\_task, n?)\}, wait\_snd := wait\_snd \oplus  \{(running\_task, que?)\}] \land  (st \in  TASK \land  \lnot  (state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) st = state(st) \implies  (state(st), (state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) st) \in  transition) \implies  t \in  TASK \land  state(t) = ready \land  \lnot  priority(topReady!) \geq  priority(t))
\end{theorem}

\begin{zproof}[lQueueSendF\_TQT\_Lemma]
use lQueueSendF\_TQ\_Lemma;
with disabled (TaskQueue, partitionDef) prove by reduce;
instantiate rtsk\_\_0 == rtsk;
apply partitionDef to predicate \langle delayed\_task\rangle  \cat  (\langle \{running\_task\} \cup  \dom  wait\_snd\rangle  \cat  \langle \dom  wait\_rcv\rangle ) \partition  \{running\_task\} \cup  \dom  time;
with disabled (partitionDef) with enabled (disjointCat) prove;
cases;
invoke TaskQueue;
invoke Task;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
apply inPower to predicate delayed\_task \in  \power  ((state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{blocked\} \rimg );
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
with enabled (disjointCat) prove;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
instantiate e\_\_0 == e;
instantiate x\_\_0 == e;
prove;
next;
invoke TaskQueue;
invoke Task;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
apply extensionality to predicate \dom  wait\_rcv \cap  (\{running\_task\} \cup  \dom  wait\_snd) = \{\};
with enabled (disjointCat) prove;
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
instantiate x\_\_1 == x;
apply inPower to predicate \dom  wait\_rcv \in  \power  (state \inv  \limg  \{blocked\} \rimg );
instantiate e == x;
prove;
next;
invoke TaskQueue;
invoke Task;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
apply extensionality to predicate delayed\_task \cap  (\{running\_task\} \cup  (\dom  wait\_rcv \cup  \dom  wait\_snd)) = \{\};
with enabled (disjointCat) prove;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
instantiate x\_\_1 == x;
instantiate e == x;
prove;
next;
apply extensionality to predicate delayed\_task \cup  (\{running\_task\} \cup  (\dom  wait\_rcv \cup  \dom  wait\_snd)) = \{running\_task\} \cup  \dom  time;
prove;
next;
instantiate t\_\_1 == t\_\_0;
apply applyOverride to expression (time \oplus  \{(running\_task, n?)\}) t\_\_0;
split t\_\_0 = running\_task;
prove;
next;
instantiate rtsk\_\_0 == t;
prove;
next;
\end{zproof}

\begin{theorem}{QueueSendF\_TQT\_vc\_ref}
\forall  QueueSendF\_TQTFSBSig | true @ \pre  QueueSendF\_TQT
\end{theorem}

\begin{zproof}[QueueSendF\_TQT\_vc\_ref]
use findDelegate[a := state \inv  \limg  \{ready\} \rimg , g := priority];
with disabled (TaskQueueTime) prove by reduce;
instantiate running\_task' == f (state \inv  \limg  \{ready\} \rimg );
prove;
use lQueueSendF\_TQT\_Lemma[topReady! := f (state \inv  \limg  \{ready\} \rimg )];
prove;
instantiate t\_\_0 == rtsk;
prove;
with normalization rewrite;
\end{zproof}

\begin{schema}{QueueSendW\_TQT}
  \Delta TaskQueueTime\\
  QueueSendW\_TQ
\where
  clock' = clock\\
  delayed\_task' = delayed\_task\\
  time' = \{topReady!\} \ndres  time\\
  time\_slice' = time\_slice
\end{schema}

\begin{zed}
QueueSendW\_TQTFSBSig \defs TaskQueueTime \land  QueueSendW\_TQFSBSig
\end{zed}

\begin{theorem}{lQueueSendW\_TQT\_Lemma}
\forall  TaskQueueTime; topReady!: TASK; que?: QUEUE | running\_task \notin  \dom  release\_rcv \land  (running\_task \in  \dom  release\_snd \implies  que? = release\_snd(running\_task)) \land  que? \in  queue \land  q\_size(que?) < q\_max(que?) \land  topReady! \in  wait\_rcv \inv  \limg  \{que?\} \rimg  \land  (\forall  wrct: wait\_rcv \inv  \limg  \{que?\} \rimg  @ priority(topReady!) \geq  priority(wrct)) \land  priority(running\_task) \geq  priority(topReady!) @ \lnot  (TaskQueueTime[q\_size := q\_size \oplus  \{(que?, (1 + q\_size(que?)))\}, release\_rcv := release\_rcv \oplus  \{(topReady!, que?)\}, release\_snd := \{running\_task\} \ndres  release\_snd, state := state \oplus  \{(topReady!, ready)\}, time := \{topReady!\} \ndres  time, wait\_rcv := \{topReady!\} \ndres  wait\_rcv] \land  priority(topReady!) \leq  priority(running\_task) \land  (st \in  TASK \land  \lnot  (state \oplus  \{(topReady!, ready)\}) st = state(st) \implies  (state(st), (state \oplus  \{(topReady!, ready)\}) st) \in  transition) \implies  wr \in  \dom  wait\_rcv \land  wait\_rcv(wr) = que? \land  \lnot  priority(topReady!) \geq  priority(wr))
\end{theorem}

\begin{zproof}[lQueueSendW\_TQT\_Lemma]
use lQueueSendW\_TQ\_Lemma;
with disabled (TaskQueue, partitionDef) prove by reduce;
instantiate wrct\_\_0 == wrct;
apply partitionDef to predicate \langle delayed\_task\rangle  \cat  (\langle \dom  wait\_snd\rangle  \cat  \langle (\dom  wait\_rcv \setminus  \{topReady!\})\rangle ) \partition  \dom  time \setminus  \{topReady!\};
with disabled (partitionDef) with enabled (disjointCat) prove;
cases;
apply inPower to predicate delayed\_task \in  \power  ((state \oplus  \{(topReady!, ready)\}) \inv  \limg  \{blocked\} \rimg );
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
with enabled (disjointCat) prove;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
instantiate x == topReady!;
instantiate e\_\_0 == e;
rewrite;
next;
apply extensionality to predicate \dom  wait\_snd \cap  (\dom  wait\_rcv \setminus  \{topReady!\}) = \{\};
with enabled (disjointCat) prove;
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
instantiate x\_\_0 == x;
prove;
next;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_snd \cup  (\dom  wait\_rcv \setminus  \{topReady!\})) = \{\};
with enabled (disjointCat) prove;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
instantiate x\_\_0 == x;
prove;
next;
apply extensionality to predicate delayed\_task \cup  (\dom  wait\_snd \cup  (\dom  wait\_rcv \setminus  \{topReady!\})) = \dom  time \setminus  \{topReady!\};
with enabled (disjointCat) prove;
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
instantiate x\_\_0 == x;
instantiate x\_\_1 == x;
split x \in  delayed\_task;
prove;
split x \in  \dom  wait\_snd;
prove;
next;
instantiate t\_\_0 == t;
prove;
next;
instantiate wrct\_\_0 == wr;
prove;
next;
\end{zproof}

\begin{theorem}{QueueSendW\_TQT\_vc\_ref}
\forall  QueueSendW\_TQTFSBSig | true @ \pre  QueueSendW\_TQT
\end{theorem}

\begin{zproof}[QueueSendW\_TQT\_vc\_ref]
use findDelegate[a := wait\_rcv \inv  \limg  \{que?\} \rimg , g := priority];
with disabled (TaskQueueTime) prove by reduce;
instantiate topReady! == f (wait\_rcv \inv  \limg  \{que?\} \rimg );
prove;
use lQueueSendW\_TQT\_Lemma[topReady! := f (wait\_rcv \inv  \limg  \{que?\} \rimg )];
prove;
instantiate wr\_\_0 == f (wait\_rcv \inv  \limg  \{que?\} \rimg );
instantiate t == wrct;
with normalization rewrite;
\end{zproof}

\begin{schema}{QueueSendWS\_TQT}
  \Delta TaskQueueTime\\
  QueueSendWS\_TQ
\where
  clock' = clock\\
  delayed\_task' = delayed\_task\\
  time' = \{topReady!\} \ndres  time\\
  time\_slice' = time\_slice
\end{schema}

\begin{zed}
QueueSendWS\_TQTFSBSig \defs TaskQueueTime \land  QueueSendWS\_TQFSBSig
\end{zed}

\begin{theorem}{lQueueSendWS\_TQT\_Lemma}
\forall  TaskQueueTime; topReady!: TASK; que?: QUEUE | running\_task \notin  \dom  release\_rcv \land  (running\_task \in  \dom  release\_snd \implies  que? = release\_snd(running\_task)) \land  que? \in  queue \land  q\_size(que?) < q\_max(que?) \land  topReady! \in  wait\_rcv \inv  \limg  \{que?\} \rimg  \land  (\forall  wrct: wait\_rcv \inv  \limg  \{que?\} \rimg  @ priority(topReady!) \geq  priority(wrct)) \land  priority(topReady!) > priority(running\_task) @ \lnot  (TaskQueueTime[log\_context := log\_context \oplus  \{(running\_task, phys\_context)\}, phys\_context := log\_context(topReady!), q\_size := q\_size \oplus  \{(wait\_rcv(topReady!), (1 + q\_size (wait\_rcv(topReady!))))\}, release\_rcv := release\_rcv \oplus  \{(topReady!, wait\_rcv(topReady!))\}, release\_snd := \{running\_task\} \ndres  release\_snd, running\_task := topReady!, state := state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\}), time := \{topReady!\} \ndres  time, wait\_rcv := \{topReady!\} \ndres  wait\_rcv] \land  (st \in  TASK \land  \lnot  (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) st = state(st) \implies  (state(st), (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) st) \in  transition) \implies  wr \in  \dom  wait\_rcv \land  wait\_rcv(wr) = wait\_rcv(topReady!) \land  \lnot  priority(topReady!) \geq  priority(wr))
\end{theorem}

\begin{zproof}[lQueueSendWS\_TQT\_Lemma]
use lQueueSendWS\_TQ\_Lemma;
with disabled (TaskQueue, partitionDef) prove by reduce;
instantiate wrct\_\_0 == wrct;
apply partitionDef to predicate \langle delayed\_task\rangle  \cat  (\langle \dom  wait\_snd\rangle  \cat  \langle (\dom  wait\_rcv \setminus  \{topReady!\})\rangle ) \partition  \dom  time \setminus  \{topReady!\};
with disabled (partitionDef) with enabled (disjointCat) prove;
cases;
apply inPower to predicate delayed\_task \in  \power  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{blocked\} \rimg );
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
with enabled (disjointCat) prove;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
instantiate e\_\_0 == e;
instantiate x == e;
invoke TaskQueue;
invoke Task;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
prove;
next;
apply extensionality to predicate \dom  wait\_snd \cap  (\dom  wait\_rcv \setminus  \{topReady!\}) = \{\};
with enabled (disjointCat) prove;
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
instantiate x\_\_0 == x;
prove;
next;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_snd \cup  (\dom  wait\_rcv \setminus  \{topReady!\})) = \{\};
with enabled (disjointCat) prove;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
instantiate x\_\_0 == x;
prove;
next;
apply extensionality to predicate delayed\_task \cup  (\dom  wait\_snd \cup  (\dom  wait\_rcv \setminus  \{topReady!\})) = \dom  time \setminus  \{topReady!\};
with enabled (disjointCat) prove;
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
instantiate x\_\_0 == x;
instantiate x\_\_1 == x;
split x \in  delayed\_task;
prove;
split x \in  \dom  wait\_snd;
prove;
next;
instantiate t\_\_0 == t;
prove;
next;
instantiate wrct\_\_0 == wr;
prove;
next;
\end{zproof}

\begin{theorem}{QueueSendWS\_TQT\_vc\_ref}
\forall  QueueSendWS\_TQTFSBSig | true @ \pre  QueueSendWS\_TQT
\end{theorem}

\begin{zproof}[QueueSendWS\_TQT\_vc\_ref]
with disabled (TaskQueueTime) prove by reduce;
instantiate running\_task' == topReady!;
prove;
use lQueueSendWS\_TQT\_Lemma;
prove;
instantiate wr\_\_0 == wrct;
prove;
with normalization rewrite;
\end{zproof}

\begin{zed}
QueueSend\_TQT \defs QueueSendN\_TQT \lor  QueueSendF\_TQT \lor  QueueSendW\_TQT \lor  QueueSendWS\_TQT
\end{zed}

\begin{zed}
QueueReceiveN\_TQT \defs ExtendTaskQueueXi \land  QueueReceiveN\_TQ
\end{zed}

\begin{zed}
QueueReceiveN\_TQTFSBSig \defs TaskQueueTime \land  QueueReceiveN\_TQFSBSig
\end{zed}

\begin{theorem}{QueueReceiveN\_TQT\_vc\_ref}
\forall  QueueReceiveN\_TQTFSBSig | true @ \pre  QueueReceiveN\_TQT
\end{theorem}

\begin{zproof}[QueueReceiveN\_TQT\_vc\_ref]
use QueueReceiveN\_TQ\_vc\_ref;
with disabled (TaskQueue) prove by reduce;
\end{zproof}

\begin{schema}{QueueReceiveE\_TQT}
  \Delta TaskQueueTime\\
  QueueReceiveE\_TQ\\
  n?: \nat 
\where
  n? > clock\\
  clock' = clock\\
  delayed\_task' = delayed\_task\\
  time' = time \oplus  \{(running\_task \mapsto  n?)\}\\
  time\_slice' = time\_slice
\end{schema}

\begin{schema}{QueueReceiveE\_TQTFSBSig}
  TaskQueueTime\\
  QueueReceiveE\_TQFSBSig\\
  n?: \nat 
\where
  n? > clock
\end{schema}

\begin{theorem}{lQueueReceiveE\_TQT\_Lemma}
\forall  TaskQueueTime; que?: QUEUE; topReady!: TASK; n?: \nat  | running\_task \notin  \dom  release\_snd \land  (running\_task \in  \dom  release\_rcv \implies  que? = release\_rcv(running\_task)) \land  que? \in  queue \land  q\_size(que?) = 0 \land  running\_task \neq  idle \land  topReady! \in  state \inv  \limg  \{ready\} \rimg  \land  (\forall  rtsk: state \inv  \limg  \{ready\} \rimg  @ priority(topReady!) \geq  priority(rtsk)) \land  n? > clock @ \lnot  (TaskQueueTime[log\_context := log\_context \oplus  \{(running\_task, phys\_context)\}, phys\_context := log\_context(topReady!), release\_rcv := \{running\_task\} \ndres  release\_rcv, running\_task := topReady!, state := state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\}), time := time \oplus  \{(running\_task, n?)\}, wait\_rcv := wait\_rcv \oplus  \{(running\_task, que?)\}] \land  (st \in  TASK \land  \lnot  (state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) st = state(st) \implies  (state(st), (state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) st) \in  transition) \implies  t \in  TASK \land  state(t) = ready \land  \lnot  priority(topReady!) \geq  priority(t))
\end{theorem}

\begin{zproof}[lQueueReceiveE\_TQT\_Lemma]
use lQueueReceiveE\_TQ\_Lemma;
with disabled (TaskQueue, partitionDef) prove by reduce;
instantiate rtsk\_\_0 == rtsk;
apply partitionDef to predicate \langle delayed\_task\rangle  \cat  (\langle \dom  wait\_snd\rangle  \cat  \langle (\{running\_task\} \cup  \dom  wait\_rcv)\rangle ) \partition  \{running\_task\} \cup  \dom  time;
with disabled (partitionDef) with enabled (disjointCat) prove;
cases;
invoke TaskQueue;
invoke Task;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
apply inPower to predicate delayed\_task \in  \power  ((state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{blocked\} \rimg );
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
prove;
instantiate e\_\_0 == e;
prove;
next;
invoke TaskQueue;
invoke Task;
apply extensionality to predicate \dom  wait\_snd \cap  (\{running\_task\} \cup  \dom  wait\_rcv) = \{\};
with enabled (disjointCat) prove;
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
instantiate x\_\_1 == x;
apply inPower to predicate \dom  wait\_snd \in  \power  (state \inv  \limg  \{blocked\} \rimg );
instantiate e == x;
prove;
next;
invoke TaskQueue;
invoke Task;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
apply extensionality to predicate delayed\_task \cap  (\{running\_task\} \cup  (\dom  wait\_rcv \cup  \dom  wait\_snd)) = \{\};
with enabled (disjointCat) prove;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
instantiate x\_\_1 == x;
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
instantiate e == x;
prove;
next;
apply extensionality to predicate delayed\_task \cup  (\{running\_task\} \cup  (\dom  wait\_rcv \cup  \dom  wait\_snd)) = \{running\_task\} \cup  \dom  time;
prove;
next;
instantiate t\_\_1 == t\_\_0;
apply applyOverride to expression (time \oplus  \{(running\_task, n?)\}) t\_\_0;
split t\_\_0 = running\_task;
prove;
next;
instantiate rtsk\_\_0 == t;
prove;
next;
\end{zproof}

\begin{theorem}{QueueReceiveE\_TQT\_vc\_ref}
\forall  QueueReceiveE\_TQTFSBSig | true @ \pre  QueueReceiveE\_TQT
\end{theorem}

\begin{zproof}[QueueReceiveE\_TQT\_vc\_ref]
use findDelegate[a := state \inv  \limg  \{ready\} \rimg , g := priority];
with disabled (TaskQueueTime) prove by reduce;
instantiate running\_task' == f (state \inv  \limg  \{ready\} \rimg );
prove;
use lQueueReceiveE\_TQT\_Lemma[topReady! := f (state \inv  \limg  \{ready\} \rimg )];
prove;
instantiate t\_\_0 == rtsk;
prove;
with normalization rewrite;
\end{zproof}

\begin{schema}{QueueReceiveW\_TQT}
  \Delta TaskQueueTime\\
  QueueReceiveW\_TQ
\where
  clock' = clock\\
  delayed\_task' = delayed\_task\\
  time' = \{topReady!\} \ndres  time\\
  time\_slice' = time\_slice
\end{schema}

\begin{zed}
QueueReceiveW\_TQTFSBSig \defs TaskQueueTime \land  QueueReceiveW\_TQFSBSig
\end{zed}

\begin{theorem}{lQueueReceiveW\_TQT\_Lemma}
\forall  TaskQueueTime; que?: QUEUE; topReady!: TASK | running\_task \notin  \dom  release\_snd \land  (running\_task \in  \dom  release\_rcv \implies  que? = release\_rcv(running\_task)) \land  que? \in  queue \land  q\_size(que?) > 0 \land  topReady! \in  wait\_snd \inv  \limg  \{que?\} \rimg  \land  (\forall  wsnt: wait\_snd \inv  \limg  \{que?\} \rimg  @ priority(topReady!) \geq  priority(wsnt)) \land  priority(running\_task) \geq  priority(topReady!) @ \lnot  (TaskQueueTime[q\_size := q\_size \oplus  \{(que?, (q\_size(que?) - 1))\}, release\_rcv := \{running\_task\} \ndres  release\_rcv, release\_snd := release\_snd \oplus  \{(topReady!, que?)\}, state := state \oplus  \{(topReady!, ready)\}, time := \{topReady!\} \ndres  time, wait\_snd := \{topReady!\} \ndres  wait\_snd] \land  priority(topReady!) \leq  priority(running\_task) \land  (st \in  TASK \land  \lnot  (state \oplus  \{(topReady!, ready)\}) st = state(st) \implies  (state(st), (state \oplus  \{(topReady!, ready)\}) st) \in  transition) \implies  ws \in  \dom  wait\_snd \land  wait\_snd(ws) = que? \land  \lnot  priority(topReady!) \geq  priority(ws))
\end{theorem}

\begin{zproof}[lQueueReceiveW\_TQT\_Lemma]
use lQueueReceiveW\_TQ\_Lemma;
with disabled (TaskQueue, partitionDef) prove by reduce;
instantiate wsnt\_\_0 == wsnt;
apply partitionDef to predicate \langle delayed\_task\rangle  \cat  (\langle \dom  wait\_snd \setminus  \{topReady!\}\rangle  \cat  \langle \dom  wait\_rcv\rangle ) \partition  \dom  time \setminus  \{topReady!\};
with disabled (partitionDef) with enabled (disjointCat) prove;
cases;
apply inPower to predicate delayed\_task \in  \power  ((state \oplus  \{(topReady!, ready)\}) \inv  \limg  \{blocked\} \rimg );
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
with enabled (disjointCat) prove;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
instantiate x == e;
instantiate e\_\_0 == e;
prove;
next;
apply extensionality to predicate \dom  wait\_rcv \cap  (\dom  wait\_snd \setminus  \{topReady!\}) = \{\};
with enabled (disjointCat) prove;
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
instantiate x\_\_0 == x;
prove;
next;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  (\dom  wait\_snd \setminus  \{topReady!\})) = \{\};
with enabled (disjointCat) prove;
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
instantiate x\_\_0 == x;
instantiate x\_\_1 == x;
prove;
next;
apply extensionality to predicate delayed\_task \cup  (\dom  wait\_rcv \cup  (\dom  wait\_snd \setminus  \{topReady!\})) = \dom  time \setminus  \{topReady!\};
with enabled (disjointCat) prove;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
instantiate x\_\_0 == x;
instantiate x\_\_1 == x;
split x \in  delayed\_task;
prove;
split x \in  \dom  wait\_rcv;
prove;
next;
instantiate t\_\_0 == t;
prove;
next;
instantiate wsnt\_\_0 == ws;
prove;
next;
\end{zproof}

\begin{theorem}{QueueReceiveW\_TQT\_vc\_ref}
\forall  QueueReceiveW\_TQTFSBSig | true @ \pre  QueueReceiveW\_TQT
\end{theorem}

\begin{zproof}[QueueReceiveW\_TQT\_vc\_ref]
use findDelegate[a := wait\_snd \inv  \limg  \{que?\} \rimg , g := priority];
with disabled (TaskQueueTime) prove by reduce;
instantiate topReady! == f (wait\_snd \inv  \limg  \{que?\} \rimg );
prove;
use lQueueReceiveW\_TQT\_Lemma[topReady! := f (wait\_snd \inv  \limg  \{que?\} \rimg )];
prove;
instantiate ws\_\_0 == f (wait\_snd \inv  \limg  \{que?\} \rimg );
instantiate t == wsnt;
with normalization rewrite;
\end{zproof}

\begin{schema}{QueueReceiveWS\_TQT}
  \Delta TaskQueueTime\\
  QueueReceiveWS\_TQ
\where
  clock' = clock\\
  delayed\_task' = delayed\_task\\
  time' = \{topReady!\} \ndres  time\\
  time\_slice' = time\_slice
\end{schema}

\begin{zed}
QueueReceiveWS\_TQTFSBSig \defs TaskQueueTime \land  QueueReceiveWS\_TQFSBSig
\end{zed}

\begin{theorem}{lQueueReceiveWS\_TQT\_Lemma}
\forall  TaskQueueTime; que?: QUEUE; topReady!: TASK | running\_task \notin  \dom  release\_snd \land  (running\_task \in  \dom  release\_rcv \implies  que? = release\_rcv(running\_task)) \land  que? \in  queue \land  q\_size(que?) > 0 \land  topReady! \in  wait\_snd \inv  \limg  \{que?\} \rimg  \land  (\forall  wsnt: wait\_snd \inv  \limg  \{que?\} \rimg  @ priority(topReady!) \geq  priority(wsnt)) \land  priority(topReady!) > priority(running\_task) @ \lnot  (TaskQueueTime[log\_context := log\_context \oplus  \{(running\_task, phys\_context)\}, phys\_context := log\_context(topReady!), q\_size := q\_size \oplus  \{(wait\_snd(topReady!), (q\_size (wait\_snd(topReady!)) - 1))\}, release\_rcv := \{running\_task\} \ndres  release\_rcv, release\_snd := release\_snd \oplus  \{(topReady!, wait\_snd(topReady!))\}, running\_task := topReady!, state := state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\}), time := \{topReady!\} \ndres  time, wait\_snd := \{topReady!\} \ndres  wait\_snd] \land  (st \in  TASK \land  \lnot  (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) st = state(st) \implies  (state(st), (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) st) \in  transition) \implies  ws \in  \dom  wait\_snd \land  wait\_snd(ws) = wait\_snd(topReady!) \land  \lnot  priority(topReady!) \geq  priority(ws))
\end{theorem}

\begin{zproof}[lQueueReceiveWS\_TQT\_Lemma]
use lQueueReceiveWS\_TQ\_Lemma;
with disabled (TaskQueue, partitionDef) prove by reduce;
apply partitionDef to predicate \langle delayed\_task\rangle  \cat  (\langle \dom  wait\_snd \setminus  \{topReady!\}\rangle  \cat  \langle \dom  wait\_rcv\rangle ) \partition  \dom  time \setminus  \{topReady!\};
instantiate wsnt\_\_0 == wsnt;
with disabled (partitionDef) with enabled (disjointCat) prove;
cases;
invoke TaskQueue;
invoke Task;
apply inPower to predicate delayed\_task \in  \power  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{blocked\} \rimg );
with enabled (disjointCat) prove;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
instantiate e\_\_0 == e;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
instantiate x\_\_0 == e;
prove;
next;
apply extensionality to predicate \dom  wait\_rcv \cap  (\dom  wait\_snd \setminus  \{topReady!\}) = \{\};
with enabled (disjointCat) prove;
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
instantiate x\_\_0 == x;
prove;
next;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  (\dom  wait\_snd \setminus  \{topReady!\})) = \{\};
with enabled (disjointCat) prove;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
instantiate x\_\_0 == x;
instantiate x\_\_1 == x;
prove;
next;
apply extensionality to predicate delayed\_task \cup  (\dom  wait\_rcv \cup  (\dom  wait\_snd \setminus  \{topReady!\})) = \dom  time \setminus  \{topReady!\};
with enabled (disjointCat) prove;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
instantiate x\_\_0 == x;
instantiate x\_\_1 == x;
split x \in  delayed\_task;
prove;
split x \in  \dom  wait\_rcv;
prove;
next;
instantiate t\_\_0 == t;
prove;
next;
instantiate wsnt\_\_0 == ws;
prove;
next;
\end{zproof}

\begin{theorem}{QueueReceiveWS\_TQT\_vc\_ref}
\forall  QueueReceiveWS\_TQTFSBSig | true @ \pre  QueueReceiveWS\_TQT
\end{theorem}

\begin{zproof}[QueueReceiveWS\_TQT\_vc\_ref]
with disabled (TaskQueueTime) prove by reduce;
instantiate running\_task' == topReady!;
prove;
use lQueueReceiveWS\_TQT\_Lemma;
prove;
instantiate ws\_\_0 == wsnt;
prove;
with normalization rewrite;
\end{zproof}

\begin{zed}
QueueReceive\_TQT \defs QueueReceiveN\_TQT \lor  QueueReceiveE\_TQT \lor  QueueReceiveW\_TQT \lor  QueueReceiveWS\_TQT
\end{zed}

\begin{schema}{DelayUntil\_TQT}
  \Delta TaskQueueTime\\
  n?: \nat \\
  topReady!: TASK
\where
  running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv\\
  state(topReady!) = ready\\
  running\_task \neq  idle\\
  \forall  t: TASK | state(t) = ready @ priority(topReady!) \geq  priority(t)\\
  n? > clock\\
  \exists  st?: STATE | st? = blocked @ Reschedule[topReady!/target?, tasks/tasks?, priority/pri?]\\
  \Xi Queue\\
  clock' = clock\\
  delayed\_task' = delayed\_task \cup  \{running\_task\}\\
  time' = time \oplus  \{(running\_task \mapsto  n?)\}\\
  time\_slice' = time\_slice
\end{schema}

\begin{schema}{DelayUntil\_TQTFSBSig}
  TaskQueueTime\\
  n?: \nat 
\where
  running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv\\
  running\_task \neq  idle\\
  n? > clock
\end{schema}

\begin{theorem}{lDelayUntil\_TQT\_Lemma}
\forall  TaskQueueTime; n?: \nat ; topReady!: TASK | running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv \land  running\_task \neq  idle \land  state(topReady!) = ready \land  n? > clock \land  (\forall  rtsk: state \inv  \limg  \{ready\} \rimg  @ priority(topReady!) \geq  priority(rtsk)) @ \lnot  (TaskQueueTime[delayed\_task := delayed\_task \cup  \{running\_task\}, log\_context := log\_context \oplus  \{(running\_task, phys\_context)\}, phys\_context := log\_context(topReady!), running\_task := topReady!, state := state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\}), time := time \oplus  \{(running\_task, n?)\}] \land  (st \in  TASK \land  \lnot  (state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) st = state(st) \implies  (state(st), (state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) st) \in  transition) \implies  t \in  TASK \land  state(t) = ready \land  \lnot  priority(topReady!) \geq  priority(t))
\end{theorem}

\begin{zproof}[lDelayUntil\_TQT\_Lemma]
with disabled (partitionDef) prove by reduce;
apply partitionDef to predicate \langle delayed\_task \cup  (state \inv  \limg  \{running\} \rimg )\rangle  \cat  (\langle \dom  wait\_snd\rangle  \cat  \langle \dom  wait\_rcv\rangle ) \partition  \dom  time \cup  (state \inv  \limg  \{running\} \rimg );
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
with disabled (partitionDef) with enabled (disjointCat) prove;
cases;
apply inPower to predicate delayed\_task \in  \power  ((state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{blocked\} \rimg );
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
with enabled (disjointCat) prove;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
instantiate e\_\_0 == e;
instantiate x\_\_0 == e;
prove;
next;
apply extensionality to predicate TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ) = \{running\_task\} \cup  (\{topReady!\} \cup  (TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg )));
prove;
with normalization rewrite;
next;
apply extensionality to predicate (state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{running\} \rimg  = \{topReady!\};
prove;
instantiate x\_\_0 == x;
apply applyOverride to expression (state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) x;
prove;
with normalization rewrite;
next;
apply inPower to predicate \dom  wait\_snd \in  \power  ((state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{blocked\} \rimg );
apply inPower to predicate \dom  wait\_snd \in  \power  (state \inv  \limg  \{blocked\} \rimg );
prove;
instantiate e\_\_0 == e;
prove;
next;
apply inPower to predicate \dom  wait\_rcv \in  \power  ((state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{blocked\} \rimg );
apply inPower to predicate \dom  wait\_rcv \in  \power  (state \inv  \limg  \{blocked\} \rimg );
prove;
instantiate e\_\_0 == e;
prove;
next;
apply extensionality to predicate (delayed\_task \cup  (state \inv  \limg  \{running\} \rimg )) \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
with enabled (disjointCat) prove;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
instantiate x\_\_1 == x;
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
instantiate e == x;
apply inPower to predicate \dom  wait\_snd \in  \power  (state \inv  \limg  \{blocked\} \rimg );
apply inPower to predicate \dom  wait\_rcv \in  \power  (state \inv  \limg  \{blocked\} \rimg );
instantiate e\_\_0 == x;
instantiate e\_\_1 == x;
split x \in  delayed\_task;
prove;
next;
apply extensionality to predicate delayed\_task \cup  ((state \inv  \limg  \{running\} \rimg ) \cup  (\dom  wait\_rcv \cup  \dom  wait\_snd)) = \dom  time \cup  (state \inv  \limg  \{running\} \rimg );
prove;
split y \in  \dom  wait\_snd;
prove;
next;
with enabled (applyOverride) prove;
next;
instantiate rtsk == pt;
with enabled (applyOverride) prove;
split pt = running\_task;
prove;
next;
instantiate t\_\_1 == t\_\_0;
instantiate x == t;
apply applyOverride to expression (time \oplus  \{(running\_task, n?)\}) t;
split t \in  \dom  time;
with disabled (partitionDef) prove;
next;
apply applyOverride to expression (state \oplus  (\{(running\_task, blocked)\} \cup  \{(topReady!, running)\})) st;
prove;
with normalization rewrite;
next;
instantiate rtsk == t;
prove;
next;
\end{zproof}

\begin{theorem}{DelayUntil\_TQT\_vc\_ref}
\forall  DelayUntil\_TQTFSBSig | true @ \pre  DelayUntil\_TQT
\end{theorem}

\begin{zproof}[DelayUntil\_TQT\_vc\_ref]
use findDelegate[a := state \inv  \limg  \{ready\} \rimg , g := priority];
with disabled (TaskQueueTime) prove by reduce;
instantiate running\_task' == f (state \inv  \limg  \{ready\} \rimg );
prove;
use lDelayUntil\_TQT\_Lemma[topReady! := f (state \inv  \limg  \{ready\} \rimg )];
prove;
instantiate t\_\_0 == rtsk;
prove;
\end{zproof}

\begin{schema}{CheckDelayedTaskN\_TQT}
  \Delta TaskQueueTime\\
  topWaiting!: TASK
\where
  running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv\\
  topWaiting! \in  \dom  time\\
  \forall  wt: \dom  time @ time(topWaiting!) \leq  time(wt)\\
  \forall  wt: \dom  time | time(wt) = time(topWaiting!) @ priority(topWaiting!) \geq  priority(wt)\\
  priority(topWaiting!) \leq  priority(running\_task)\\
  \Xi TaskData\\
  state' = state \oplus  \{(topWaiting! \mapsto  ready)\}\\
  \Xi ContextData\\
  \Xi PrioData\\
  \Xi QueueData\\
  wait\_snd' = \{topWaiting!\} \ndres  wait\_snd\\
  wait\_rcv' = \{topWaiting!\} \ndres  wait\_rcv\\
  \Xi QReleasingData\\
  clock' = time(topWaiting!)\\
  delayed\_task' = delayed\_task \setminus  \{topWaiting!\}\\
  time' = \{topWaiting!\} \ndres  time\\
  time\_slice' = time\_slice
\end{schema}

\begin{zproof}[CheckDelayedTaskN\_TQT\$domainCheck]
prove;
\end{zproof}

\begin{schema}{CheckDelayedTaskN\_TQTFSBSig}
  TaskQueueTime
\where
  running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv\\
  \exists  topWaiting!: \dom  time @ (\forall  wt: \dom  time @ time(topWaiting!) \leq  time(wt)) \land  (\forall  wt: \dom  time | time(wt) = time(topWaiting!) @ priority(topWaiting!) \geq  priority(wt)) \land  priority(topWaiting!) \leq  priority(running\_task)
\end{schema}

\begin{zproof}[CheckDelayedTaskN\_TQTFSBSig\$domainCheck]
prove;
\end{zproof}

\begin{theorem}{lCheckDelayedTaskN\_TQT\_Lemma}
\forall  TaskQueueTime; topWaiting!: TASK | running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv \land  topWaiting! \in  \dom  time \land  (\forall  dtk: \dom  time @ time(topWaiting!) \leq  time(dtk)) \land  (\forall  detk: \dom  time | time(detk) = time(topWaiting!) @ priority(topWaiting!) \geq  priority(detk)) \land  priority(topWaiting!) \leq  priority(running\_task) @ \lnot  (TaskQueueTime[clock := time(topWaiting!), delayed\_task := delayed\_task \setminus  \{topWaiting!\}, state := state \oplus  \{(topWaiting!, ready)\}, time := \{topWaiting!\} \ndres  time, wait\_rcv := \{topWaiting!\} \ndres  wait\_rcv, wait\_snd := \{topWaiting!\} \ndres  wait\_snd] \land  (st \in  TASK \land  \lnot  (state \oplus  \{(topWaiting!, ready)\}) st = state(st) \implies  (state(st), (state \oplus  \{(topWaiting!, ready)\}) st) \in  transition) \land  (wt \in  \dom  time \implies  time(topWaiting!) \leq  time(wt)) \implies  wt\_\_0 \in  \dom  time \land  time(wt\_\_0) = time(topWaiting!) \land  \lnot  priority(topWaiting!) \geq  priority(wt\_\_0))
\end{theorem}

\begin{zproof}[lCheckDelayedTaskN\_TQT\_Lemma]
use domTime[t := topWaiting!];
with disabled (partitionDef) prove by reduce;
apply partitionDef to predicate \langle delayed\_task \setminus  \{topWaiting!\}\rangle  \cat  (\langle \dom  wait\_snd \setminus  \{topWaiting!\}\rangle  \cat  \langle (\dom  wait\_rcv \setminus  \{topWaiting!\})\rangle ) \partition  \dom  time \setminus  \{topWaiting!\};
apply extensionality to predicate TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ) = \{topWaiting!\} \cup  (TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ));
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
use applyInRanPfun[TASK, \num ][A := TASK, B := \nat , f := time, a := topWaiting!];
with disabled (partitionDef) with enabled (disjointCat, applyOverride) prove;
cases;
apply inPower to predicate delayed\_task \in  \power  (\{topWaiting!\} \cup  ((state \oplus  \{(topWaiting!, ready)\}) \inv  \limg  \{blocked\} \rimg ));
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
prove;
instantiate e\_\_0 == e;
prove;
next;
apply extensionality to predicate (\dom  wait\_rcv \setminus  \{topWaiting!\}) \cap  (\dom  wait\_snd \setminus  \{topWaiting!\}) = \{\};
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
prove;
instantiate x\_\_1 == x;
prove;
next;
apply inPower to predicate \ran  (\{topWaiting!\} \ndres  wait\_snd) \in  \power  (\dom  q\_size);
apply inPower to predicate \ran  wait\_snd \in  \power  (\dom  q\_size);
prove;
instantiate e\_\_0 == e;
with enabled (inRan) prove;
instantiate x\_\_2 == x;
prove;
next;
apply inPower to predicate \ran  (\{topWaiting!\} \ndres  wait\_rcv) \in  \power  (\dom  q\_size);
apply inPower to predicate \ran  wait\_rcv \in  \power  (\dom  q\_size);
prove;
instantiate e\_\_0 == e;
with enabled (inRan) prove;
instantiate x\_\_2 == x;
prove;
next;
apply extensionality to predicate (\dom  release\_rcv \cup  \dom  release\_snd) \cap  (\dom  wait\_rcv \setminus  \{topWaiting!\} \cup  (\dom  wait\_snd \setminus  \{topWaiting!\})) = \{\};
apply extensionality to predicate (\dom  release\_rcv \cup  \dom  release\_snd) \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
prove;
instantiate x\_\_1 == x;
instantiate x\_\_2 == x;
prove;
next;
apply inPower to predicate \dom  wait\_snd \in  \power  (\{topWaiting!\} \cup  ((state \oplus  \{(topWaiting!, ready)\}) \inv  \limg  \{blocked\} \rimg ));
apply inPower to predicate \dom  wait\_snd \in  \power  (state \inv  \limg  \{blocked\} \rimg );
prove;
instantiate e\_\_0 == e;
prove;
next;
apply inPower to predicate \dom  wait\_rcv \in  \power  (\{topWaiting!\} \cup  ((state \oplus  \{(topWaiting!, ready)\}) \inv  \limg  \{blocked\} \rimg ));
apply inPower to predicate \dom  wait\_rcv \in  \power  (state \inv  \limg  \{blocked\} \rimg );
prove;
instantiate e\_\_0 == e;
prove;
next;
apply extensionality to predicate (delayed\_task \setminus  \{topWaiting!\}) \cap  (\dom  wait\_rcv \setminus  \{topWaiting!\} \cup  (\dom  wait\_snd \setminus  \{topWaiting!\})) = \{\};
with enabled (disjointCat) prove;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
instantiate x\_\_1 == x;
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
instantiate x\_\_1 == x;
prove;
next;
apply extensionality to predicate delayed\_task \setminus  \{topWaiting!\} \cup  (\dom  wait\_rcv \setminus  \{topWaiting!\} \cup  (\dom  wait\_snd \setminus  \{topWaiting!\})) = \dom  time \setminus  \{topWaiting!\};
prove;
next;
with normalization rewrite;
next;
instantiate pt\_\_0 == pt;
apply applyOverride to expression (state \oplus  \{(topWaiting!, ready)\}) pt;
prove;
with normalization rewrite;
next;
instantiate dtk == t;
prove;
next;
invoke transition;
rewrite;
next;
instantiate dtk == wt;
prove;
next;
instantiate detk == wt\_\_0;
prove;
next;
\end{zproof}

\begin{theorem}{CheckDelayedTaskN\_TQT\_vc\_ref}
\forall  CheckDelayedTaskN\_TQTFSBSig | true @ \pre  CheckDelayedTaskN\_TQT
\end{theorem}

\begin{zproof}[CheckDelayedTaskN\_TQT\_vc\_ref]
with disabled (TaskQueueTime) prove by reduce;
instantiate topWaiting\_\_0! == topWaiting!;
prove;
use lCheckDelayedTaskN\_TQT\_Lemma;
prove;
instantiate wt\_\_1 == dtk;
instantiate wt\_\_2 == detk;
with normalization rewrite;
\end{zproof}

\begin{schema}{CheckDelayedTaskS\_TQT}
  \Delta TaskQueueTime\\
  topWaiting!: TASK
\where
  running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv\\
  topWaiting! \in  \dom  time\\
  \forall  wt: \dom  time @ time(topWaiting!) \leq  time(wt)\\
  \forall  wt: \dom  time | time(wt) = time(topWaiting!) @ priority(topWaiting!) \geq  priority(wt)\\
  priority(topWaiting!) > priority(running\_task)\\
  \exists  st?: STATE | st? = ready @ Reschedule[topWaiting!/target?, tasks/tasks?, priority/pri?]\\
  \Xi QueueData\\
  wait\_snd' = \{topWaiting!\} \ndres  wait\_snd\\
  wait\_rcv' = \{topWaiting!\} \ndres  wait\_rcv\\
  \Xi QReleasingData\\
  clock' = time(topWaiting!)\\
  delayed\_task' = delayed\_task \setminus  \{topWaiting!\}\\
  time' = \{topWaiting!\} \ndres  time\\
  time\_slice' = time\_slice
\end{schema}

\begin{zproof}[CheckDelayedTaskS\_TQT\$domainCheck]
prove;
\end{zproof}

\begin{schema}{CheckDelayedTaskS\_TQTFSBSig}
  TaskQueueTime
\where
  running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv\\
  \exists  topWaiting!: \dom  time @ (\forall  wt: \dom  time @ time(topWaiting!) \leq  time(wt)) \land  (\forall  wt: \dom  time | time(wt) = time(topWaiting!) @ priority(topWaiting!) \geq  priority(wt)) \land  priority(topWaiting!) > priority(running\_task)
\end{schema}

\begin{zproof}[CheckDelayedTaskS\_TQTFSBSig\$domainCheck]
prove;
\end{zproof}

\begin{theorem}{lCheckDelayedTaskS\_TQT\_Lemma}
\forall  TaskQueueTime; topWaiting!: TASK | running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv \land  topWaiting! \in  \dom  time \land  (\forall  dtk: \dom  time @ time(topWaiting!) \leq  time(dtk)) \land  (\forall  detk: \dom  time | time(detk) = time(topWaiting!) @ priority(topWaiting!) \geq  priority(detk)) \land  priority(topWaiting!) > priority(running\_task) @ \lnot  (TaskQueueTime[clock := time(topWaiting!), delayed\_task := delayed\_task \setminus  \{topWaiting!\}, log\_context := log\_context \oplus  \{(running\_task, phys\_context)\}, phys\_context := log\_context(topWaiting!), running\_task := topWaiting!, state := state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\}), time := \{topWaiting!\} \ndres  time, wait\_rcv := \{topWaiting!\} \ndres  wait\_rcv, wait\_snd := \{topWaiting!\} \ndres  wait\_snd] \land  (st \in  TASK \land  \lnot  (state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) st = state(st) \implies  (state(st), (state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) st) \in  transition) \land  (wt \in  \dom  time \implies  time(topWaiting!) \leq  time(wt)) \implies  wt\_\_0 \in  \dom  time \land  time(wt\_\_0) = time(topWaiting!) \land  \lnot  priority(topWaiting!) \geq  priority(wt\_\_0))
\end{theorem}

\begin{zproof}[lCheckDelayedTaskS\_TQT\_Lemma]
use domTime[t := topWaiting!];
with disabled (partitionDef) prove by reduce;
apply partitionDef to predicate \langle delayed\_task \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{running\} \rimg )\rangle  \cat  (\langle \dom  wait\_snd \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{running\} \rimg )\rangle  \cat  \langle (\dom  wait\_rcv \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{running\} \rimg ))\rangle ) \partition  \dom  time \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{running\} \rimg );
with disabled (partitionDef) with enabled (disjointCat) prove;
cases;
apply inPower to predicate delayed\_task \in  \power  (\{topWaiting!\} \cup  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{blocked\} \rimg ));
with enabled (disjointCat) prove;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
instantiate e\_\_0 == e;
prove;
next;
apply extensionality to predicate TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ) = \{topWaiting!\} \cup  (TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ) \cup  (state \inv  \limg  \{running\} \rimg ));
prove;
with normalization rewrite;
next;
apply extensionality to predicate (state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{running\} \rimg  = \{topWaiting!\};
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
prove;
instantiate x\_\_0 == x;
apply applyOverride to expression (state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) x;
with normalization prove;
next;
apply extensionality to predicate (\dom  wait\_rcv \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{running\} \rimg )) \cap  (\dom  wait\_snd \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{running\} \rimg )) = \{\};
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
prove;
instantiate x\_\_0 == x;
rewrite;
next;
apply inPower to predicate \ran  (((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{running\} \rimg ) \ndres  wait\_snd) \in  \power  (\dom  q\_size);
apply inPower to predicate \ran  wait\_snd \in  \power  (\dom  q\_size);
prove;
instantiate e\_\_0 == e;
with enabled (inRan) prove;
instantiate x\_\_0 == x;
prove;
next;
apply inPower to predicate \ran  (((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{running\} \rimg ) \ndres  wait\_rcv) \in  \power  (\dom  q\_size);
apply inPower to predicate \ran  wait\_rcv \in  \power  (\dom  q\_size);
prove;
instantiate e\_\_0 == e;
with enabled (inRan) prove;
instantiate x\_\_0 == x;
prove;
next;
apply extensionality to predicate (\dom  release\_rcv \cup  \dom  release\_snd) \cap  (\dom  wait\_rcv \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{running\} \rimg ) \cup  (\dom  wait\_snd \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{running\} \rimg ))) = \{\};
apply extensionality to predicate (\dom  release\_rcv \cup  \dom  release\_snd) \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
prove;
instantiate x\_\_0 == x;
prove;
next;
apply inPower to predicate \dom  wait\_snd \in  \power  (((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{blocked\} \rimg ) \cup  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{running\} \rimg ));
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
with enabled (disjointCat) prove;
apply inPower to predicate \dom  wait\_snd \in  \power  (state \inv  \limg  \{blocked\} \rimg );
instantiate e\_\_0 == e;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
instantiate x\_\_0 == e;
with enabled (applyOverride) prove;
next;
apply inPower to predicate \dom  wait\_rcv \in  \power  (((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{blocked\} \rimg ) \cup  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{running\} \rimg ));
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
with enabled (disjointCat) prove;
apply inPower to predicate \dom  wait\_rcv \in  \power  (state \inv  \limg  \{blocked\} \rimg );
instantiate e\_\_0 == e;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
instantiate x\_\_0 == e;
with enabled (applyOverride) prove;
next;
use applyInRanPfun[TASK, \num ][A := TASK, B := \nat , f := time, a := topWaiting!];
prove;
next;
instantiate t\_\_0 == topWaiting!;
prove;
next;
apply extensionality to predicate (delayed\_task \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{running\} \rimg )) \cap  (\dom  wait\_rcv \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{running\} \rimg ) \cup  (\dom  wait\_snd \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{running\} \rimg ))) = \{\};
with enabled (disjointCat) prove;
apply extensionality to predicate delayed\_task \cap  (\dom  wait\_rcv \cup  \dom  wait\_snd) = \{\};
apply extensionality to predicate \dom  wait\_rcv \cap  \dom  wait\_snd = \{\};
instantiate x\_\_0 == x;
instantiate x\_\_1 == x;
prove;
next;
apply extensionality to predicate delayed\_task \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{running\} \rimg ) \cup  (\dom  wait\_rcv \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{running\} \rimg ) \cup  (\dom  wait\_snd \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{running\} \rimg ))) = \dom  time \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topWaiting!, running)\})) \inv  \limg  \{running\} \rimg );
prove;
next;
with enabled (applyOverride) prove;
split idle = running\_task;
prove;
next;
instantiate pt\_\_0 == pt;
split pt \in  TASK;
with enabled (applyOverride) prove;
with normalization rewrite;
next;
instantiate dtk == t;
prove;
next;
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
instantiate x == st;
with enabled (applyOverride) prove;
with normalization rewrite;
next;
instantiate dtk == wt;
prove;
next;
instantiate detk == wt\_\_0;
prove;
next;
\end{zproof}

\begin{theorem}{CheckDelayedTaskS\_TQT\_vc\_ref}
\forall  CheckDelayedTaskS\_TQTFSBSig | true @ \pre  CheckDelayedTaskS\_TQT
\end{theorem}

\begin{zproof}[CheckDelayedTaskS\_TQT\_vc\_ref]
with disabled (TaskQueueTime) prove by reduce;
instantiate running\_task' == topWaiting!;
prove;
use lCheckDelayedTaskS\_TQT\_Lemma;
prove;
instantiate wt\_\_1 == dtk;
instantiate wt\_\_2 == detk;
with normalization rewrite;
\end{zproof}

\begin{schema}{TimeSlicing\_TQT}
  \Delta TaskQueueTime\\
  topReady!: TASK
\where
  running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv\\
  state(topReady!) = ready\\
  priority(topReady!) = priority(running\_task)\\
  \forall  t: \dom  time @ time\_slice \leq  time(t)\\
  \exists  st?: STATE | st? = ready @ Reschedule[topReady!/target?, tasks/tasks?, priority/pri?]\\
  \Xi Queue\\
  clock' = clock\\
  delayed\_task' = delayed\_task\\
  time' = time\\
  time\_slice' = time\_slice + slice\_delay
\end{schema}

\begin{zproof}[TimeSlicing\_TQT\$domainCheck]
 prove by reduce;
\end{zproof}

\begin{schema}{TimeSlicing\_TQTFSBSig}
  TaskQueueTime
\where
  running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv\\
  \forall  t: \dom  time @ time\_slice \leq  time(t)\\
  \exists  topReady!: state \inv  \limg  \{ready\} \rimg  @ priority(topReady!) = priority(running\_task)
\end{schema}

\begin{zproof}[TimeSlicing\_TQTFSBSig\$domainCheck]
 prove by reduce;
\end{zproof}

\begin{theorem}{lTimeSlicing\_TQT\_Lemma}
\forall  TaskQueueTime; topReady!: TASK | running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv \land  state(topReady!) = ready \land  priority(topReady!) = priority(running\_task) \land  (\forall  ts: \dom  time @ time\_slice \leq  time(ts)) @ \lnot  (TaskQueueTime[log\_context := log\_context \oplus  \{(running\_task, phys\_context)\}, phys\_context := log\_context(topReady!), running\_task := topReady!, state := state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\}), time\_slice := time\_slice + slice\_delay] \implies  st \in  TASK \land  \lnot  (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) st = state(st) \land  \lnot  (state(st), (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) st) \in  transition)
\end{theorem}

\begin{zproof}[lTimeSlicing\_TQT\_Lemma]
prove by reduce;
apply extensionality to predicate TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg ) = TASK \setminus  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{nonexistent\} \rimg );
apply extensionality to predicate state \inv  \limg  \{running\} \rimg  = \{running\_task\};
prove;
cases;
apply inPower to predicate delayed\_task \in  \power  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{blocked\} \rimg );
apply inPower to predicate delayed\_task \in  \power  (state \inv  \limg  \{blocked\} \rimg );
prove;
instantiate e\_\_0 == e;
prove;
next;
apply extensionality to predicate (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{running\} \rimg  = \{topReady!\};
prove;
instantiate x\_\_0 == x;
apply applyOverride to expression (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) x;
with normalization rewrite;
next;
apply inPower to predicate \dom  wait\_snd \in  \power  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{blocked\} \rimg );
prove;
apply inPower to predicate \dom  wait\_snd \in  \power  (state \inv  \limg  \{blocked\} \rimg );
instantiate e\_\_0 == e;
prove;
next;
apply inPower to predicate \dom  wait\_rcv \in  \power  ((state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) \inv  \limg  \{blocked\} \rimg );
prove;
apply inPower to predicate \dom  wait\_rcv \in  \power  (state \inv  \limg  \{blocked\} \rimg );
instantiate e\_\_0 == e;
prove;
next;
use slice\_delay\_def;
prove;
next;
with enabled (applyOverride) prove;
with normalization rewrite;
next;
with enabled (applyOverride) prove;
with normalization rewrite;
next;
instantiate pt\_\_0 == pt;
use applyInRanFun[TASK, \nat ][f := priority, a := pt];
with enabled (applyOverride) prove;
with normalization rewrite;
next;
apply applyOverride to expression (state \oplus  (\{(running\_task, ready)\} \cup  \{(topReady!, running)\})) st;
prove;
with normalization rewrite;
next;
\end{zproof}

\begin{theorem}{TimeSlicing\_TQT\_vc\_ref}
\forall  TimeSlicing\_TQTFSBSig | true @ \pre  TimeSlicing\_TQT
\end{theorem}

\begin{zproof}[TimeSlicing\_TQT\_vc\_ref]
with disabled (TaskQueueTime) prove by reduce;
instantiate running\_task' == topReady!;
prove;
use lTimeSlicing\_TQT\_Lemma;
prove;
instantiate t == ts;
prove;
\end{zproof}

\begin{schema}{NoSlicing\_TQT}
  \Delta TaskQueueTime
\where
  running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv\\
  \forall  t: \dom  time @ time\_slice \leq  time(t)\\
  \forall  t: state \inv  \limg  \{ready\} \rimg  @ priority(t) < priority(running\_task)\\
  \Xi Task\\
  \Xi Queue\\
  clock' = clock\\
  delayed\_task' = delayed\_task\\
  time' = time\\
  time\_slice' = time\_slice + slice\_delay
\end{schema}

\begin{zproof}[NoSlicing\_TQT\$domainCheck]
prove;
\end{zproof}

\begin{schema}{NoSlicing\_TQTFSBSig}
  TaskQueueTime
\where
  running\_task \notin  \dom  release\_snd \cup  \dom  release\_rcv\\
  \forall  t: \dom  time @ time\_slice \leq  time(t)\\
  \forall  t: state \inv  \limg  \{ready\} \rimg  @ priority(t) < priority(running\_task)
\end{schema}

\begin{zproof}[NoSlicing\_TQTFSBSig\$domainCheck]
prove;
\end{zproof}

\begin{theorem}{NoSlicing\_TQT\_vc\_ref}
\forall  NoSlicing\_TQTFSBSig | true @ \pre  NoSlicing\_TQT
\end{theorem}

\begin{zproof}[NoSlicing\_TQT\_vc\_ref]
use slice\_delay\_def;
prove by reduce;
\end{zproof}

\end{document}